## Stream: new members

### Topic: Filters

#### Valery Isaev (May 12 2020 at 00:22):

I heard that analysis and topology in Lean is implemented using filters which are supposed to be more convenient from formalization point of view. I'd like to know what are advantages of this approach compared to the ordinary way of doing things.

#### Johan Commelin (May 12 2020 at 04:46):

@Valery Isaev Patrick wrote a nice short discussion in our perfectoid paper: https://math.commelin.net/files/poplws20cpp_perfectoid.pdf

#### Johan Commelin (May 12 2020 at 04:47):

You will want section 4

#### Kevin Buzzard (May 12 2020 at 06:08):

I think Johannes Hoelzl ported a lot of the basic results from Isabelle, following a book by I James. Hoelzl might well have written the Isabelle code as well

#### Patrick Massot (May 12 2020 at 09:39):

The first step is to read the module docstring at https://leanprover-community.github.io/mathlib_docs/order/filter/basic.html. Then indeed there should be stuff in the perfectoid paper (I already started to forgot what's in there exactly). The book by James is "Topologies and uniformities". PM me if you have difficulties finding it

#### Rob Lewis (May 12 2020 at 09:40):

I see a badly formed doc string there!

#### Patrick Massot (May 12 2020 at 09:40):

Also note that the new book Mathematics in Lean will eventually contain explanations about you need to know here

#### Patrick Massot (May 12 2020 at 09:41):

Rob Lewis said:

I see a badly formed doc string there!

#### Valery Isaev (May 12 2020 at 22:50):

Thanks for the references. If I understand correctly, the advantage is that various notions of limits are defined in terms of filters and hence the same lemmas and definitions can be used to establish the basic theory for them.

#### Kevin Buzzard (May 12 2020 at 23:26):

As a mathematician the advantages I see to filters are pretty much what you say: I can say "this sequence of reals tends to 7", "this sequence of reals diverges to +infinity", "this continuous function of x tends to 7 as x tends to 37", "this continuous function tends to 0 as x tends to -infinity" etc. But my impression is that there are other advantages too.

#### Kevin Buzzard (May 12 2020 at 23:26):

Note in particular this very general "tendsto" predicate; I think that this was one of the key insights.

Last updated: May 06 2021 at 22:13 UTC