Formally Verified Waffle Maker (Nov 24 2020 at 07:13):
Is there a specific reason that - definitions of limits are not in mathlib? If not, I am open to sharing the definitions I wrote.
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
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.
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