## Stream: maths

### Topic: notation for limits

#### Kevin Buzzard (Nov 15 2019 at 23:49):

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 (Nov 15 2019 at 23:50):

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 (Nov 15 2019 at 23:51):

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

#### Kevin Buzzard (Nov 16 2019 at 00:06):

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

Last updated: May 06 2021 at 19:30 UTC