# Zulip Chat Archive

## Stream: maths

### Topic: filter bases

#### Patrick Massot (Mar 12 2019 at 15:25):

@Johannes Hölzl Bourbaki is always using filter bases everywhere, and it's been puzzling me forever that this seems to be nowhere in mathlib. In particular I can't find:

import order.filter open filter set lemma generate_of_base {α : Type*} {ι : Type*} {s : ι → set α} [inhabited ι] (H : ∀ i j, ∃ k, s k ⊆ s i ∩ s j) (U : set α): U ∈ generate (range s) ↔ ∃ i, s i ⊆ U := begin split ; intro h, { induction h with U U_in U V U_gen UV U_union U V U_gen V_gen U_union V_union, { rcases U_in with ⟨i, rfl⟩, use i }, { use default ι, exact (univ_mem_sets : univ ∈ principal (s $ default ι))}, { cases U_union with i Ui, use i, exact subset.trans Ui UV }, { cases U_union with i Ui, cases V_union with j Vj, cases H i j with k k_sub, use k, cases subset_inter_iff.1 k_sub with ki kj, exact subset_inter_iff.2 ⟨subset.trans ki Ui, subset.trans kj Vj⟩ }}, { cases h with i Ui, exact generate_sets.superset (generate_sets.basic $ mem_range_self i) Ui }, end

What is the story here? Do you have a better way?

#### Patrick Massot (Mar 12 2019 at 15:27):

I know this is a fake tactic mode proof, but I don't dare writing the proof term...

#### Johannes Hölzl (Mar 12 2019 at 15:27):

I usually reduce it to the infimum.

#### Johannes Hölzl (Mar 12 2019 at 15:28):

So `nhds`

is not defined using a generating set, but as a infimum of `principal`

filters. The advantage is that for the infimum very generic rules exist

#### Patrick Massot (Mar 12 2019 at 15:28):

I can also prove that, under the same assumption, `generate (range s) = ⨅ i, principal (s i)`

. But what do you gain from expressing it as the RHS?

#### Patrick Massot (Mar 12 2019 at 15:29):

I think the problem is that `⨅ i, principal (s i)`

is not very nice in general

#### Johannes Hölzl (Mar 12 2019 at 15:29):

often `s`

is not only indexed by one value, but many values. this fits nicely with `infi`

.

#### Patrick Massot (Mar 12 2019 at 15:29):

You need to take intersections of finite subsets

#### Johannes Hölzl (Mar 12 2019 at 15:30):

it is not nice if you directly work on sets, instead of on filters.

#### Johannes Hölzl (Mar 12 2019 at 15:30):

Of course, it is often hard to use filters in their full generality but when we can they are very powerful.

#### Patrick Massot (Mar 12 2019 at 15:31):

I still don't understand why the condition `H : ∀ i j, ∃ k, s k ⊆ s i ∩ s j`

appears nowhere. Whatever the language, things will always be simpler under this assumption, right?

#### Patrick Massot (Mar 12 2019 at 15:31):

This is a `directed`

something assumption

#### Johannes Hölzl (Mar 12 2019 at 15:32):

Everybody here wants to have more category theory, but nobody is using the complete lattices structure on the filters. But you can see the `infi`

as a nice behaving limit of filters. And many operations commute _somehow_ with infi.

#### Patrick Massot (Mar 12 2019 at 15:32):

`principal`

doesn't commute nicely

#### Johannes Hölzl (Mar 12 2019 at 15:33):

What you proved is essentially `mem_infi`

#### Johannes Hölzl (Mar 12 2019 at 15:33):

`tendsto`

and `principal`

and `infi`

work very nicely together!

#### Patrick Massot (Mar 12 2019 at 15:34):

`⨅ i, principal (s i)`

is *not* `principal (⨅ i, s i)`

, right?

#### Johannes Hölzl (Mar 12 2019 at 15:34):

Look at these rules: https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean#L1205

#### Johannes Hölzl (Mar 12 2019 at 15:34):

Look ma no `directed`

proof necessary :-)

#### Johannes Hölzl (Mar 12 2019 at 15:35):

Ah sorry, I didn't mean `prinicpal`

and `infi`

are commuting. But `tendsto`

and `infi`

are nice behaving

#### Patrick Massot (Mar 12 2019 at 15:35):

But the story of filter bases and sub-bases is precisely the story of `⨅ i, principal (s i)`

vs `generate (range s)`

#### Johannes Hölzl (Mar 12 2019 at 15:37):

Yes, but `generate`

only allows me to construct a filter from sets. While `⨅`

allows me to constructa filter from other filters (hence including sets)

#### Johannes Hölzl (Mar 12 2019 at 15:39):

Many statements are actually filter inclusion statements. Often they are not seen to be obvious filter inclusions, but when they are then we can use the powerful complete lattice structure.

#### Johannes Hölzl (Mar 12 2019 at 15:40):

An example is: https://github.com/leanprover-community/mathlib/commit/a4afa904f2e902e34764ff69ec5baf31ad56525a#diff-2f853d294b8568321089942e42ccd7b1L1411

Here the `directed`

proof is completely unnecessary

#### Johannes Hölzl (Mar 12 2019 at 15:42):

Or this change:

https://github.com/leanprover-community/mathlib/commit/a4afa904f2e902e34764ff69ec5baf31ad56525a#diff-11d4223aa3461ef9e12d2f034e79d0f1R375

Here the same proof which was done before `set`

-wise is now done on filters and their order structure (even when the final goal is to reduce a filer statement to a set statement)

#### Johannes Hölzl (Mar 12 2019 at 15:42):

What I want to say: `generate`

is much more limited than using `infi`

. With `infi`

we get nice compositional behaviour, and especially for the reduction of `tendsto`

statements it can be very powerful.

#### Johannes Hölzl (Mar 12 2019 at 15:44):

We can reduce `generate`

to `infi`

but not the other way round

#### Johannes Hölzl (Mar 12 2019 at 15:45):

We can define `infi`

using `generate`

, but then we lose the compositional behaviour

#### Patrick Massot (Mar 12 2019 at 15:53):

Thanks, I'll try to keep all that in mind

#### Patrick Massot (Apr 05 2020 at 12:23):

In mathlib, we have Yury's filter bases which are predicate based, and used in some places, but notably *not* in topology.bases. In the perfectoid project, we had filter bases everywhere, but we used a much more bundled approach because:

- We needed to enforce many properties of our bases
- We needed to construct filters starting from a basis having a lot of properties (typically providing a basis for neighborhood of zero in a ring that will ensure there is a topological ring structure inducing that filter).

As a scaled down example, I'd like to discuss the following example:

structure decreasing_enumerated_basis {α : Type*} (f : filter α) := (V : ℕ → set α) (in_filter : ∀ n, V n ∈ f) (decreasing : ∀ {n m}, n ≤ m → V m ⊆ V n) (basis : ∀ s, s ∈ f ↔ ∃ n, V n ⊆ s) instance {α : Type*} {f : filter α} : has_coe_to_fun (decreasing_enumerated_basis f) := ⟨_, λ B n, B.V n⟩ lemma decreasing_enumerated_basis.tendsto {α : Type*} {β : Type*} {f : filter α} {g : filter β} (B : decreasing_enumerated_basis g) (φ : α → β) : tendsto φ f g ↔ ∀ n, ∀ᶠ x in f, φ x ∈ B n := begin split ; intro h, { intro n, exact h (B.in_filter n) }, { intros s s_in, cases (B.basis s).mp s_in with n hn, apply mem_sets_of_superset (h n), exact preimage_mono hn } end lemma decreasing_enumerated_basis.tendsto' {β : Type*} {g : filter β} (B : decreasing_enumerated_basis g) {φ : ℕ → β} (h : ∀ n, φ n ∈ B n) : tendsto φ at_top g := begin rw B.tendsto, intro n, rw eventually_at_top, use n, intros m hm, exact B.decreasing hm (h m), end def decreasing_enumerated_basis.of_has_countable_basis {α : Type*} {f : filter α} (hf : has_countable_basis f) : decreasing_enumerated_basis f := ...

This setup is very convenient to use because you can apply the function defined at the bottom of this snippet, and access all the lemmas using the dot notation. What do @Sebastien Gouezel and @Yury G. Kudryashov think about this?

#### Sebastien Gouezel (Apr 05 2020 at 13:18):

If this is useful in your specific setup, then go for it! Although I would formulate the third property in your structure using Yury's predicate and call it `has_basis`

, to get all the existing lemmas for bases with `B.has_basis.foo`

.

#### Patrick Massot (Apr 05 2020 at 13:36):

Yes, this is obviously the good solution.

#### Gabriel Ebner (Apr 05 2020 at 14:06):

In January, Yury said that he has already migrated `has_countable_basis`

to the new API and that he's just splitting it up into multiple PRs. https://github.com/leanprover-community/mathlib/pull/1896#issuecomment-576681341

#### Patrick Massot (Apr 05 2020 at 14:19):

Actually maybe an even better solution would be to wrap `filter.has_basis`

into a structure and have more specific basis extending it. That would save a couple of restatements.

#### Patrick Massot (Apr 05 2020 at 21:08):

@Yury G. Kudryashov and @Sebastien Gouezel I'd like comments on WIP at https://github.com/leanprover-community/mathlib/commit/94701f1a9f33abbeb17894929d567affd42e2267. There I did three things: first I removed the filter countable basis stuff from `topology.bases`

and put it in `order.filter.bases`

, next to `filter.has_basis`

where I can be later refactord. Then I added my `decreasing_enumerated_basis`

, in the same file. And then my end goal in this story is what I added in `topology.sequences`

. There is general stuff about subsequences, the high scores stuff and the final lemma which was the end-goal:

variables {X : Type*} [topological_space X] [first_countable_topology X] lemma compact.tendsto_subseq {s : set X} {u : ℕ → X} (hs : compact s) (hu : ∀ n, u n ∈ s) : ∃ (x ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ tendsto (u ∘ φ) at_top (𝓝 x) := hs.tendsto_subseq' (univ_mem_sets' hu)

I still need to clean a bit the last file, but I'd like to read at least comments about the reorganization stuff, and naming suggestions.

#### Patrick Massot (Apr 05 2020 at 21:12):

The next step will be to hook this to Sébastien's proper metric space thing to actually get Bolzano-Weirstrass.

#### Yury G. Kudryashov (Apr 05 2020 at 23:27):

@Gabriel Ebner I'm afraid that I've accidentally deleted this part (messed up with `git stash`

es). So far @Patrick Massot 's approach looks very good. I think that `has_countable_basis`

should become `nonempty (decreasing_enumerated_basis f)`

if we want it in `Prop`

. BTW, I'd turn it into a `class`

because in many cases (`at_top`

on `nat`

, `nhds`

in an `emetric_space`

) it can be deduced automatically.

#### Gabriel Ebner (Apr 06 2020 at 11:42):

I don't think we make any use of the fact that `has_countable_basis`

is in Prop. It is only used as a hypothesis for lemmas. So I'd say we can replace `has_countable_basis`

by `decreasing_enumerated_basis`

directly. Although the name is quite a mouthful.

#### Patrick Massot (Apr 06 2020 at 12:00):

`has_countable_basis`

is still easier to check in principle, and also what is in the traditional sources.

#### Patrick Massot (Apr 06 2020 at 12:00):

Long names are hard to avoid, especially since we don't want cryptic abreviations.

Last updated: May 11 2021 at 16:22 UTC