# Zulip Chat Archive

## Stream: maths

### Topic: filter base

#### Yury G. Kudryashov (Jan 14 2020 at 18:25):

Hi, many simplification lemmas about filters can be formulated in terms of

def filter.has_base {α : Type*} {ι : Sort*} (f : filter α) (s : ι → set α) : Prop := ∀ {{t : set α}}, t ∈ f <-> ∃ i, s i ⊆ t

I use `s : ι → set α`

instead of `set (set α)`

because usually this base is a range of a function. This property is stronger than `f = infi (principal ∘ s)`

, and immediately implies statements like `tendsto m f f' → f.has_base s → ∀ t ∈ f', ∃ i, s i ⊆ m ⁻¹' t`

, and similarly for `f'`

.

What do you think about adding it to `mathlib`

?

#### Yury G. Kudryashov (Jan 14 2020 at 18:35):

A possible application: we can prove that various families (open balls, closed balls, same with rational `r`

, same with `r=n⁻¹`

) form bases of `nhds x`

in an `emetric/metric`

space, then use these lemmas in rewrites without proving `N²`

helper lemmas.

#### Patrick Massot (Jan 14 2020 at 20:56):

We already had this need in the perfectoid project, but it's among the many things that should be PRed but are not. We also tried several implementations and I'm super happy with the one we currently have. See https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/filter.lean#L82 and the rest of that file, as well as https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/topological_groups.lean, https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/for_mathlib/topological_rings.lean etc. One difficulty is to make something that we can easily use in more specialized situation without rewriting all lemmas to make them really usable.

#### Yury G. Kudryashov (Jan 14 2020 at 22:04):

Why did you choose to have a separate type instead of a predicate? I think that usually we already have a filter and want to rewrite some `tendsto`

in a more reasonable way.

#### Patrick Massot (Jan 14 2020 at 22:08):

That's not the case in the perfectoid project. The filter base comes first, then the filter and then the topology.

#### Patrick Massot (Jan 14 2020 at 22:09):

#### Patrick Massot (Jan 14 2020 at 22:09):

But I didn't find a nice way to cover all use cases.

#### Mario Carneiro (Jan 14 2020 at 22:59):

Isn't there already a `filter.generate`

function for generating a filter from a filter (sub)base?

#### Mario Carneiro (Jan 14 2020 at 22:59):

I can certainly see the use in a `has_base`

predicate for saying that a filter is generated by a base other than the one used in its definition though

Last updated: May 18 2021 at 06:15 UTC