Zulip Chat Archive

Stream: maths

Topic: epsilon delta limit definitions

view this post on Zulip Formally Verified Waffle Maker (Nov 24 2020 at 07:13):

Is there a specific reason that ε\varepsilon-δ\delta definitions of limits are not in mathlib? If not, I am open to sharing the definitions I wrote.

view this post on Zulip Kevin Buzzard (Nov 24 2020 at 07:31):

It's because if they were there then people would ask for epsilon-N definitions of other limits and then one sided limits and then the definition of a sequence tending to +infinity and etc etc, and then someone would realise that a beautiful way to do everything at once would be to use filters and then they'd all get changed to filters and we'd be back where we started

view this post on Zulip Johan Commelin (Nov 24 2020 at 07:32):

@Formally Verified Waffle Maker In https://www.youtube.com/watch?v=hhOPRaR3tx0 @Patrick Massot explains this in detail.

view this post on Zulip Sebastien Gouezel (Nov 24 2020 at 07:41):

Also, it's there, see docs#metric.tendsto_nhds_nhds

Last updated: May 14 2021 at 18:28 UTC