notation for limits

Stream: maths

[Kevin Buzzard]

import data.real.basic

notation `|` x `|` := abs x
definition is_limit (a : ℕ → ℝ) (l : ℝ) := ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N ≤ n → |a n - l| < ε

I'd like to have some good notation for limits in Lean 3.4.2 or 3.5. Something as near to $\operatorname{lim}_{n\to\infty}a_n=\ell$ as possible. Any suggestions?

[Kevin Buzzard]

One issue is that "limit" isn't a function, it's really a predicate on a pair consisting of a sequence and a real number. The fact that for any sequence there's at most one real number which can be its limit is cool but I'm not exactly sure how to build it in.

[Chris Hughes]

There's already a lim function on cau_seq in mathlib.

[Kevin Buzzard]

Oh thanks. But what I'm really interested in is the notation.