## 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):

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