Origin: `example (a : ℕ → ℝ) (ha : ∀ n, a n = (n + 1) / n) : ∃ L, SeqLim a L := by` To Be: `example (a : ℕ → ℝ) (ha : ∀ n > 0, a n = (n + 1) / n) : ∃ L, SeqLim a L := by` Otherwise, `a n` is not well-defined at `n=0`
Origin:
example (a : ℕ → ℝ) (ha : ∀ n, a n = (n + 1) / n) : ∃ L, SeqLim a L := byTo Be:
example (a : ℕ → ℝ) (ha : ∀ n > 0, a n = (n + 1) / n) : ∃ L, SeqLim a L := byOtherwise,
a nis not well-defined atn=0