El reto de esta semana consiste en demostrar en Lean 4 que la sucesión constante (a_{n} = L) converge a (L). Para ello, completar la siguiente teoría:

import Mathlib.Tactic

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

variable {a : ℕ → ℝ}
variable {L : ℝ}

example
  (h : ∀ n, a n = L)
  : LimSuc a L :=
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.