Prove that the constant sequence \(a_{n} = L\) converges to \(L\).

To do this, complete the following theory:

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

How to publish your solution?

1. Write your proof in live.lean-lang.org and copy the generated link.
2. Post it on the Mastodon thread for this problem, with a message like:
   "My solution is at [link]."
3. You will be able to compare your approach with other participants during the week. The official solution will be published next Monday.