Skip to main content

Reto 22: Subsucesiones con límites distintos implican no convergencia

El reto de esta semana consiste en demostrar en Lean 4 que si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. Para ello, completar la siguiente teoría:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

-- a converge a L
def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε

-- La sucesión a es convergente
def SucConvergente (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

-- φ es una función de extracción.
def extraccion (φ : ℕ → ℕ) : Prop :=
  StrictMono φ

-- b es una subsucesión de a.
def subsucesion (b a : ℕ → ℝ) : Prop :=
  ∃ φ, extraccion φ ∧ b = a ∘ φ

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ M : ℝ}

example
  (hb₁ : subsucesion b₁ a)
  (hL₁ : LimSuc b₁ L₁)
  (hb₂ : subsucesion b₂ a)
  (hL₂ : LimSuc b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SucConvergente a :=
by sorry

¿Cómo publicar tu solución?

  1. Escribe tu demostración en live.lean-lang.org y copia el enlace que genera.
  2. Publícalo en el hilo de Mastodon de este problema, con un mensaje del tipo:
    «Mi solución está en [enlace].»
  3. Podrás comparar tu planteamiento con el de otros participantes durante la semana. La solución oficial se publicará el próximo lunes.