delta/epsilon notion of continuity

Stream: new members

[Alex Meiburg]

If I have (f : ℝ → ℝ) (hf₂ : Continuous f), how do I get the standard epsilon-delta notion of continuity on "f"? I loogled for a good fifteen minutes and couldn't find it. And so I tried looking at existing proofs that involves continuous real functions because surely one of them had this fact, like sin or cosine and so on, but they all just proof continuity from the fact that f is an order-preserving isomorphism.

The actual definition of continuity is the (less familiar for analysis, more powerful and general) one involving filters and neighborhoods -- and I'm sure there's a "simple" way to turn that into a statement about neighborhoods in R and so get the eps-delta statement, but that involves looking up a bunnnnch more lemmas and so on and seems much harder.

[David Renshaw]

Here's how I've done it: https://github.com/dwrensha/compfiles/blob/2a454827870259167c77c91116392000ca3df722/Compfiles/Romania1998P12.lean#L49-L55
There may be a simpler way.

[David Renshaw]

Metric.continuous_iff'.mp then Filter.eventually_iff.mp then mem_nhds_iff.mp then Metric.isOpen_iff.mp

[Alex Meiburg]

Hmm, alright. Well, it seems like something that should be in mathlib, so fingers crossed -- but otherwise those 4 lines aren't too bad I guess. Thanks. :)

[Alex Meiburg]

Also, extend_function_mono seems like a nice lemma that should be in mathlib

[Alex Meiburg]

(except that I would write the conclusion of that lemma as just u = f by funext.)

[Anatole Dedecker]

Is docs#Metric.continuous_iff what you want?

[Alex Meiburg]

Yes :face_palm: I don't know why that was so hard to find...

[Anatole Dedecker]

Don't blame yourself for not finding such a thing, blame our searching tools!

[Jireh Loreaux]

However, if you look at the proof of docs#Metric.tendsto_nhds_nhds, you can get a better idea of how to go from the filter definition to the "more familiar" versions of limits in general.