Zulip Chat Archive

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 limnan=\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: Dec 20 2023 at 11:08 UTC