product metric space

Stream: maths

[Patrick Massot]

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]

@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]

I guess you need to add parenthesis around ⨅

[Patrick Massot]

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]

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]

Doh! Adding parenthesis works indeed!

[Patrick Massot]

I wonder how Lean could parse the version without parenthesis

[Chris Hughes]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Chris Hughes]

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]

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

[Johannes Hölzl]

of course, this is an important instance!

[Chris Hughes]

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