Una subsucesión se obtiene aplicando a la sucesión original una función de extracción; es decir, una función \(φ : ℕ \to ℕ\) estrictamente creciente. Por ejemplo, la subsucesión \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] se obtiene con la función de extracción \(\varphi\) definida por \(\varphi(n) = 2n\).

Las definiciones anteriores se formalizan en Lean 4 como:

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

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

-- a es el límite de u.
def LimSuc (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

El reto de esta semana consiste en demostrar en Lean 4 que toda subsucesión de una sucesión convergente converge al mismo límite que la sucesión. Para ello, completar la siguiente teoría de Lean 4:

import Mathlib.Data.Real.Basic

variable {u v : ℕ → ℝ}
variable {a : ℝ}

def extraccion (φ : ℕ → ℕ):=
  StrictMono φ

def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ

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

example
  (hv : subsucesion v u)
  (ha : LimSuc u a)
  : LimSuc v 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.