## Stream: Is there code for X?

### Topic: How can one represent Calculus limits using filters?

#### Formally Verified Waffle Maker (Dec 15 2020 at 06:26):

I have been trying to learn about filters by looking at their usages in mathlib, but I still find them difficult. I was wondering how can one represent $\displaystyle\lim_{x \to 3} 2x$, for instance, using filters? Representing limits using filters would also serve as a great resource for beginners to Lean and mathlib.

#### Floris van Doorn (Dec 15 2020 at 06:34):

The default way to talk about filters in mathlib is the predicate that a limit is a certain value. This is called docs#filter.tendsto.

#### Floris van Doorn (Dec 15 2020 at 06:35):

With that, you can represent your instance (over the reals) as

import analysis.specific_limits

open filter
example : tendsto (λ x : ℝ, 2 * x) (nhds 3) (nhds 6) :=
sorry


docs#nhds is the neighborhood filter.

#### Floris van Doorn (Dec 15 2020 at 06:36):

Or if you want to be fancy

import analysis.specific_limits

open filter
open_locale topological_space
example : tendsto (λ x : ℝ, 2 * x) (𝓝 2) (𝓝 6) :=
sorry


#### Formally Verified Waffle Maker (Dec 15 2020 at 06:37):

Floris van Doorn said:

With that, you can represent your instance (over the reals) as

import analysis.specific_limits

open filter
example : tendsto (λ x : ℝ, 2 * x) (nhds 3) (nhds 6) :=
sorry


docs#nhds is the neighborhood filter.

Thank you so much. Since the limit example you gave really helped, I think beginners to Lean would find it very helpful if that was added to the official documentation.

#### Formally Verified Waffle Maker (Dec 15 2020 at 06:42):

And I am open to helping write documentation for beginners to Lean who know Calculus, if that is something that the Lean community is interested in.

#### Johan Commelin (Dec 15 2020 at 06:46):

@Formally Verified Waffle Maker sure! you could make a PR that adds

## Example

Filters can be used to represent limits as follows ... blabla

import analysis.specific_limits

open filter
example : tendsto (λ x : ℝ, 2 * x) (nhds 3) (nhds 6) :=
sorry



to the module docstring at the top of https://leanprover-community.github.io/mathlib_docs/topology/basic.html

#### Bryan Gin-ge Chen (Dec 15 2020 at 06:49):

P.S. the proof of the example is not too hard with a few tactics:

import analysis.specific_limits

open filter
example : tendsto (λ x : ℝ, 2 * x) (nhds 3) (nhds 6) :=
by convert continuous.tendsto _ _; [norm_num, continuity]


#### Bryan Gin-ge Chen (Dec 15 2020 at 06:50):

Though maybe this is overkill.

#### Floris van Doorn (Dec 15 2020 at 06:58):

I made a PR here: leanprover-community/leanprover-community.github.io#151

#### Patrick Massot (Dec 15 2020 at 08:37):

I still intend to write the corresponding chapter of MIL one day.

#### Patrick Massot (Dec 15 2020 at 08:45):

I've started an experiment about this. This year I'm officially teaching an algebra course to very good third year students (at ENS Paris-Saclay). These students are frustrated because their curriculum doesn't include a proper course in general topology (they have a detailed course about metric spaces spaces). Some of them repeatedly asked me to teach them general topology. Last week I accepted and gave a first underground topology course by night on our BigBlueButton server. It means I'm totally free to teach it my way and students are free to leave at any time. I couldn't resist running an experiment. So, after some introduction, I started with 20 minutes about lattices and Galois connections, then I moved to filters for about one hour and only after that I defined topological spaces. I'm pretty pleased about how it went and students seemed very happy. We'll see how many come back in Week 2. I'll tell you when I'll move to uniform spaces and Bourbaki real numbers. Note that I didn't use Lean, this is a much sneakier way to sell formalized maths than what I do with my first year undergrads.

#### Kevin Buzzard (Dec 15 2020 at 09:08):

This is great. You can even tell them it's the traditional French style. You should set a problem sheet in Lean with some carefully-chosen questions which are nice to do and stick it up on a github site and then make a link to the community web editor and set it as a challenge. For example could one prove step through the Tychonoff proof using ultrafilters in a painless way in Lean?

Do we have in Lean that in a compact Hausdorff space there's a unique uniform structure compatible with the topology?

My memories of the undergraduate course I took was that continuous image of compact is compact, compact subspace of Hausdorff is closed, and closed subset of compact is compact were some pretty cool theorems. I still remember the open set proofs well. Are there slick filter proofs of these?

#### Patrick Massot (Dec 15 2020 at 09:39):

docs#compact_space_uniformity

#### Patrick Massot (Dec 15 2020 at 09:40):

https://github.com/leanprover-community/mathlib/blob/a959718e33ebb02ff61ca19220d2d33e0baae314/src/topology/subset_properties.lean#L447-L460

#### Patrick Massot (Dec 15 2020 at 09:41):

docs#is_closed.compact

#### Patrick Massot (Dec 15 2020 at 09:42):

docs#is_compact.is_closed

#### Patrick Massot (Dec 15 2020 at 09:42):

I will cover all this of course. At some point I will probably show some Lean as well, but I didn't want to reveal all weirdness at once.

Last updated: May 07 2021 at 21:10 UTC