epsilon delta limit definitions

Stream: maths

[Formally Verified Waffle Maker]

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.

[Kevin Buzzard]

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]

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

[Sebastien Gouezel]

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