# Zulip Chat Archive

## Stream: maths

### Topic: product metric space

#### Patrick Massot (Mar 04 2019 at 17:45):

Does anyone understand why the following fails (both the uncommented line and the commented one):

import topology.metric_space.basic open filter universes u v variables {ι : Type u} {α : ι → Type v} [fintype ι] [∀ i, metric_space (α i)] example : ⨅ (ε : ℝ) (h : ε>0), principal {p : (Π i, α i)×(Π i, α i) | dist p.1 p.2 < ε} = ⨅ i : ι, filter.comap (λ a : (Π i, α i)×(Π i, α i), (a.1 i, a.2 i)) uniformity := begin apply le_antisymm, -- The next line type-checks but then `apply this` fails --have := @le_antisymm (filter $ (Π i, α i)×(Π i, α i)) (@filter.partial_order ((Π i, α i)×(Π i, α i))), sorry end

#### Patrick Massot (Mar 04 2019 at 17:47):

@Johannes Hölzl I guess you are the expert here. I'm trying to relate product metric space to product topology and uniform structure.

#### Johannes Hölzl (Mar 04 2019 at 17:48):

I guess you need to add parenthesis around ⨅

#### Patrick Massot (Mar 04 2019 at 17:51):

More precisely, I already have:

section open filter lattice universe u variables {ι : Type*} (α : ι → Type u) [U : Πi, uniform_space (α i)] include U instance Pi.uniform_space : uniform_space (Πi, α i) := ⨆i, uniform_space.comap (λ a, a i) (U i) lemma pi.uniformity : @uniformity (Π i, α i) _ = ⨅ i : ι, filter.comap (λ a, (a.1 i, a.2 i)) uniformity := supr_uniformity lemma pi.uniform_continuous_proj (i : ι) : uniform_continuous (λ (a : Π (i : ι), α i), a i) := begin rw uniform_continuous_iff, apply le_supr (λ j, uniform_space.comap (λ (a : Π (i : ι), α i), a j) (U j)) end lemma pi.uniform_space_topology : (Pi.uniform_space α).to_topological_space = Pi.topological_space := to_topological_space_supr instance pi.complete [∀ i, complete_space (α i)] : complete_space (Π i, α i) := ⟨begin intros f hf, have : ∀ i, ∃ x : α i, filter.map (λ a : Πi, α i, a i) f ≤ nhds x, { intro i, have key : cauchy (map (λ (a : Π (i : ι), α i), a i) f), from cauchy_map (pi.uniform_continuous_proj α i) hf, exact (cauchy_iff_exists_le_nhds $ map_ne_bot hf.1).1 key }, choose x hx using this, use x, rw [show nhds x = (⨅i, comap (λa, a i) (nhds (x i))), by rw pi.uniform_space_topology ; exact nhds_pi, le_infi_iff], exact λ i, map_le_iff_le_comap.mp (hx i), end⟩ end

although I know Johannes will not like this instance so it should be a def (because in case iota is not finite this is not necessarily the uniform structure you are interested in). Still, I'd like these lemmas to prove that a (finite) product of complete metric spaces is complete.

#### Chris Hughes (Mar 04 2019 at 17:51):

`apply this`

fails because `this`

is an equality, and the goal is `le`

? If I get rid of `apply_le_antisymm`

it works

#### Patrick Massot (Mar 04 2019 at 17:52):

Doh! Adding parenthesis works indeed!

#### Patrick Massot (Mar 04 2019 at 17:52):

I wonder how Lean could parse the version without parenthesis

#### Chris Hughes (Mar 04 2019 at 17:53):

It didn't parse for me. It couldn't find a has_Inf instance for `Sort `

#### Patrick Massot (Mar 04 2019 at 17:54):

Now I need to think about actually proving this (but Johannes or Sébastien or anyone else is very welcome to do it while I take care of the laundry)

#### Chris Hughes (Mar 04 2019 at 17:55):

It parses if I make it a lemma. Prop is a complete lattice I guess.

#### Patrick Massot (Mar 04 2019 at 17:56):

Ooohh... It was indeed a lemma in my file

#### Chris Hughes (Mar 04 2019 at 18:00):

lemma h : (⨅ (ε : ℝ) (h : ε > 0), principal {p : (Π i, α i) × (Π i, α i) | dist p.1 p.2 < ε} = ⨅ i : ι, filter.comap (λ a : (Π i, α i)×(Π i, α i), (a.1 i, a.2 i)) uniformity) = ∀ (ε : ℝ) (h : ε > 0), principal {p : (Π i, α i) × (Π i, α i) | dist p.1 p.2 < ε} = ⨅ i : ι, filter.comap (λ a : (Π i, α i)×(Π i, α i), (a.1 i, a.2 i)) uniformity := by simp [lattice.infi_Prop_eq]

#### Patrick Massot (Mar 04 2019 at 18:01):

I can totally see Johannes not resisting the pleasure of defining this lattice instance

#### Johannes Hölzl (Mar 04 2019 at 18:05):

of course, this is an important instance!

#### Chris Hughes (Mar 04 2019 at 18:08):

I can't think of a way of defining subset without this and `pi.complete_lattice`

?

Last updated: May 09 2021 at 09:11 UTC