Zulip Chat Archive

Stream: maths

Topic: notation for limits


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 15 2019 at 23:51):

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

view this post on Zulip 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