definition of a limit

Stream: lean4

[tica]

Hello,

With lean 3 I can write write the definition very clearly.

def limit (f: ℝ → ℝ) (a: ℝ) (l: ℝ): Prop:=
  ∀ε > 0, ∃δ > 0, ∀x: ℝ, |x - a| < δ → |f x - l| < ε

How to do the same thing with lean 4?
Thanks

[Henrik Böving]

Two things:

1. To my knowledge this is not the definition of a limit used in mathlib, so if you are interested in working with mathlib you should probably stick to their definition which is filter based iirc
2. Since a limit requires real numbers and real numbers have not been defined yet in mathlib4 i'd say you don't right now, if you wait a few months or weeks however basically the same thing as above should work out in a mathlib4 project.

[tica]

Yes several definitions are usable but I try to learn to make my own definitions to learn the language.

I'm going to stay on lean 3 until the real numbers are set.

Thanks

[Winston Yin]

@tica I would recommend playing with Lean3 first, as mathlib in Lean4 is still quite bare at the moment. You may find this reference useful. Tracing chains of definitions on the mathlib3 docs site is also a good way to learn the language/library.

[tica]

Yes that is what I will do and I will learn lean 4 later.
Thanks for the reference :smile: