## Stream: maths

### Topic: epsilon delta limit definitions

#### 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.

#### 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