Zulip Chat Archive

Stream: maths

Topic: product metric space


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johannes Hölzl (Mar 04 2019 at 17:48):

I guess you need to add parenthesis around ⨅

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 04 2019 at 17:52):

Doh! Adding parenthesis works indeed!

view this post on Zulip Patrick Massot (Mar 04 2019 at 17:52):

I wonder how Lean could parse the version without parenthesis

view this post on Zulip Chris Hughes (Mar 04 2019 at 17:53):

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

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Mar 04 2019 at 17:55):

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

view this post on Zulip Patrick Massot (Mar 04 2019 at 17:56):

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

view this post on Zulip 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]

view this post on Zulip Patrick Massot (Mar 04 2019 at 18:01):

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

view this post on Zulip Johannes Hölzl (Mar 04 2019 at 18:05):

of course, this is an important instance!

view this post on Zulip 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