Demostrar que la sucesión constante \(a_{n} = L\) converge a \(L\).

Para ello, completar la siguiente teoría:

import Mathlib.Tactic

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

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

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