# Zulip Chat Archive

## Stream: maths

### Topic: filters inf inf

#### Patrick Massot (Jun 16 2018 at 11:39):

@Johannes Hölzl I have difficulties setting up my uniform space structure on topological groups. Basically the trouble is the definition involves dependent nested infimum. I tried to mimick the metric space case where you wrote:

uniformity := (⨅ ε>0, principal {p:α×α | dist p.1 p.2 < ε}),

(nested inf is somewhat hidden but still there). Question 1: would it be a good idea to rather use the subtype of positive real number as the indexing set?

#### Patrick Massot (Jun 16 2018 at 11:40):

So, in the context of a topological add group R, I wrote, with obvious notations:

uniformity := ⨅ U ∈ nhd_zero R, principal {p : R×R | p.2 - p.1 ∈ U}

#### Patrick Massot (Jun 16 2018 at 11:41):

But again this is somewhat inconvenient to use.

#### Patrick Massot (Jun 16 2018 at 11:41):

I have the following lemma, which is a restatement of something already there:

#### Patrick Massot (Jun 16 2018 at 11:41):

lemma filter.mem_sets_of_mem_infi {α : Type*} {ι : Sort*} {f : ι → filter α} {A : set α} (h : directed (≤) f) (ne : nonempty ι) : A ∈ (⨅ i,f i).sets → ∃ i, A ∈ (f i).sets := begin intro H, finish [infi_sets_eq] end

#### Patrick Massot (Jun 16 2018 at 11:42):

but already I'd like to deduced `ne`

from existence of `A`

#### Patrick Massot (Jun 16 2018 at 11:43):

And then I need a version for dependent nested inf that, I think, would be something like:

lemma filter.mem_sets_of_mem_infi' {α : Type*} {ι : Sort*} {P : ι → Prop} {f : Π i, P i → filter α} {A : set α} (H : A ∈ (⨅ i, ⨅ h : P i, f i h).sets) : ∃ i, ∃ h : P i, A ∈ (f i h).sets :=

but with some directedness assumption somewhere

#### Patrick Massot (Jun 16 2018 at 11:44):

Any help would be appreciated

#### Chris Hughes (Jun 16 2018 at 12:56):

I tried to prove it, but then realised it wasn't true.

import data.analysis.filter open set list filter lattice lemma filter.mem_sets_of_mem_infi' {α : Type*} {ι : Sort*} {P : ι → Prop} {f : Π i, P i → filter α} {A : set α} (H : A ∈ (⨅ i, ⨅ h : P i, f i h).sets) : ∃ i, ∃ h : P i, A ∈ (f i h).sets := sorry lemma proof_of_false : false := let ⟨x, hx⟩ := @filter.mem_sets_of_mem_infi' ℕ empty empty.elim (λ i, i.elim) set.univ (by simp) in x.elim

#### Chris Hughes (Jun 16 2018 at 12:57):

Not sure how helpful that is.

#### Chris Hughes (Jun 16 2018 at 13:11):

Probably need `A ≠ univ`

, because `univ`

is in every filter, but you might as well just have `nonempty ι`

, which is implied by `A ≠ univ`

,

#### Reid Barton (Jun 16 2018 at 13:17):

but already I'd like to deduced

`ne`

from existence of`A`

You should be deducing `ne`

from the fact that `f`

is directed, but I guess mathlib's definition leaves out that condition, oops.

#### Reid Barton (Jun 16 2018 at 13:32):

Apparently not assuming that a directed set is nonempty is a Bourbaki thing.

#### Reid Barton (Jun 16 2018 at 13:36):

@Patrick Massot There is

lemma infi_sets_eq' {f : β → filter α} {s : set β} (h : directed_on (λx y, f x ≤ f y) s) (ne : ∃i, i ∈ s) : (⨅ i∈s, f i).sets = (⋃ i ∈ s, (f i).sets)

#### Johannes Hölzl (Jun 16 2018 at 15:27):

Hm, I think you don't need the infimum at all, it should be possible to use `vmap`

and `nhds_zero`

:

`uniformity := vmap (fun p, p.1 - p.2) (nhds_zero R)`

#### Patrick Massot (Jun 16 2018 at 19:27):

Oh. That's a completely different start

#### Patrick Massot (Jun 16 2018 at 19:27):

But maybe it's more natural

#### Patrick Massot (Jun 16 2018 at 19:27):

It means I need to learn a completely new set of lemmas

#### Patrick Massot (Jun 16 2018 at 20:24):

It's worse than my original method

#### Patrick Massot (Jun 16 2018 at 20:24):

I can't prove any single property

#### Mario Carneiro (Jun 16 2018 at 20:25):

like what?

#### Patrick Massot (Jun 16 2018 at 20:41):

like `principal id_rel ≤ vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)`

#### Patrick Massot (Jun 16 2018 at 20:41):

and `tendsto prod.swap (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)) (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0))`

#### Patrick Massot (Jun 16 2018 at 20:42):

`filter.lift' (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)) (λ (s : set (R × R)), comp_rel s s) ≤ vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)`

#### Mario Carneiro (Jun 16 2018 at 20:42):

I assume you know `nhds_zero = nhds 0`

?

#### Patrick Massot (Jun 16 2018 at 20:42):

and `∀ (s : set R), topological_space.is_open _inst_2 s ↔ ∀ (x : R), x ∈ s → {p : R × R | p.fst = x → p.snd ∈ s} ∈ (vmap (λ (p : R × R), p.fst - p.snd) (nhds 0)).sets`

#### Patrick Massot (Jun 16 2018 at 20:43):

Johannes suggestion doesn't use `nhds_zero`

(which I defined earlier by `def nhd_zero := (nhds (0 : R)).sets`

)

#### Mario Carneiro (Jun 16 2018 at 20:44):

What do you mean? I see `nhds_zero`

in his post

#### Patrick Massot (Jun 16 2018 at 20:44):

this is based on him incorrectly guessing my definition

#### Mario Carneiro (Jun 16 2018 at 20:45):

For the first one, you have `tendsto_iff_vmap`

#### Patrick Massot (Jun 16 2018 at 20:45):

he probably thought I had `def nhd_zero := nhds (0 : R)`

#### Mario Carneiro (Jun 16 2018 at 20:45):

Well, `nhds_zero`

has a special place in the theory of top groups

#### Patrick Massot (Jun 16 2018 at 20:45):

Indeed the first thing I wrote is `rw tendsto_vmap_iff`

#### Patrick Massot (Jun 16 2018 at 20:46):

I also tried `rw tendsto_iff_vmap,`

#### Patrick Massot (Jun 16 2018 at 20:47):

but then I'm stuck

#### Mario Carneiro (Jun 16 2018 at 20:47):

then use that `-`

is continuous

#### Mario Carneiro (Jun 16 2018 at 20:47):

`continuous.tendsto`

#### Patrick Massot (Jun 16 2018 at 20:55):

I'd love to continue this discussion but I must leave at 6:30 tomorrow morning to get a plane to go to a conference in Cagliari

#### Patrick Massot (Jun 16 2018 at 20:55):

so I should sleep

#### Patrick Massot (Jun 16 2018 at 20:55):

thank you very much for these hints

#### Johannes Hölzl (Jun 17 2018 at 14:15):

I guessed `nhds_zero`

from your equation `uniformity := ⨅ U ∈ nhd_zero R, principal {p : R×R | p.2 - p.1 ∈ U}`

.

(by the way: why is it okay to call the support type of a group `R`

but not alpha?)

There are two important rules to convert between `map`

and `vmap`

: `map_le_iff_le_vmap`

, and `map_eq_vmap_of_inverse`

.

To prove the first rule use the rule `map_le_iff_le_vmap`

to move the`-`

to the left side, then using rewriting to end up with `principal {a | a = 0} = pure 0 <= nhds 0`

.

The second rule (using prod.swap): use `map_le_iff_le_vmap`

, and then `map_comp`

the left side by `(fun x, - x) o (fun p, p.1 - p.2)`

Then use `tendsto_vmap`

(together with `tendsto_comp`

).

And for the last one I guess we want to use `vmap_eq_lift'`

(which essentially proofs that your and my definition are the equal)

#### Johannes Hölzl (Jun 17 2018 at 19:43):

https://gist.github.com/johoelzl/ca90562c46b49a1bbb1be36272ec3b1a

transitivity, i.e. the `uniform_space.comp`

rule, is a little bit harder to show

#### Johannes Hölzl (Jun 17 2018 at 19:45):

Would you suggest any changes to this? if not I will just add this to mathlib

Last updated: May 09 2021 at 09:11 UTC