Working with uniformities to show separability

Stream: new members

[Josha Dekker]

Hi, for #12404 I'm trying to rework my proof of the following to allow for weaker hypotheses, but I'm not very good (= plain bad) with uniformities... does anyone have a suggestion how to proceed here?

import Mathlib

open MeasureTheory TopologicalSpace Uniformity Filter

lemma TotallyBounded.isSeparable2 {α : Type*} [UniformSpace α] [i : IsCountablyGenerated (𝓤 α)] {s : Set α} (h : TotallyBounded s) :
    TopologicalSpace.IsSeparable s:= by
  unfold TopologicalSpace.IsSeparable
  obtain ⟨x, hx⟩ := isCountablyGenerated_iff_exists_antitone_basis.mp i
  choose! f hf hfb using (fun n : ℕ => h (x n))
  use ⋃ n, f n
  have hnu : ∀ n, x n ∈ 𝓤 α := by
    intro n
    exact HasAntitoneBasis.mem hx n
  have hf := fun n => hf n (hnu n)
  have hfb := fun n => hfb n (hnu n)
  constructor
  · apply Set.countable_iUnion
    exact fun i => Set.Finite.countable (hf i)
  · intro x hx
    rw [UniformSpace.mem_closure_iff_ball]
    intro V hV
    sorry

[Josha Dekker]

Original version was

lemma TotallyBounded.isSeparable4 {α : Type*} [PseudoMetricSpace α] {s : Set α} (h : TotallyBounded s) :
    TopologicalSpace.IsSeparable s:= by
  rw [Metric.totallyBounded_iff] at h
  choose! f hf hfb using (fun n : ℕ => h (1/(n+1)) Nat.one_div_pos_of_nat)
  use ⋃ n, f n
  constructor
  · apply Set.countable_iUnion
    exact fun i => (hf i).countable
  · intro x hx
    rw [Metric.mem_closure_iff]
    intro ε hε
    obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε
    have : ∃ b ∈ f n, dist x b < ε := by
      obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hfb n hx)
      simp only [one_div, Set.mem_iUnion, Metric.mem_ball, exists_prop] at hi
      use i, hi.1
      apply lt_trans hi.2 ?_
      rw [inv_eq_one_div]
      exact hn
    aesop

[Felix Weilacher]

do you know about docs#UniformSpace.metrizableSpace ?

[Felix Weilacher]

This is actually something I've been wondering: Because of this theorem, is it ever correct to add a lemma about ``countably generated'' uniform spaces to mathlib? Or should one always just use Pseudo-metric spaces in such a case.

[Felix Weilacher]

Another question is whether this theorem should be an instance now that Lean allows loops in typeclass inference

[Josha Dekker]

No, I'm afraid I've missed that one as I was looking for something with pseudoMetrizableSpace to patch my argument.. I'll give it a try right away

[Felix Weilacher]

there is also a version for pseudo metrizability immediately prior to the theorem I linked

[Josha Dekker]

Yes, I recall what went wrong there for me when I tried the pseudo-metrizable version earlier today: Lean doesn't know that the two induced topological spaces agree

[Josha Dekker]

This is the problem (I'm sticking with pseudo metrizability so I don't need to assume it is a T0 space)

import Mathlib

open MeasureTheory TopologicalSpace Uniformity Filter

lemma TotallyBounded.isSeparable6 {α : Type*} [UniformSpace α] [i : IsCountablyGenerated (𝓤 α)] {s : Set α} (h : TotallyBounded s) :
    TopologicalSpace.IsSeparable s:= by
  have := UniformSpace.pseudoMetrizableSpace (X := α)
  have := Metric.totallyBounded_iff.mp h -- Lean doesn't know the spaces agree, so this line raises an error
  choose! f hf hfb using (fun n : ℕ => h (1/(n+1)) Nat.one_div_pos_of_nat)
  use ⋃ n, f n
  constructor
  · apply Set.countable_iUnion
    exact fun i => (hf i).countable
  · intro x hx
    rw [Metric.mem_closure_iff]
    intro ε hε
    obtain ⟨n, hn⟩ := exists_nat_one_div_lt hε
    have : ∃ b ∈ f n, dist x b < ε := by
      obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hfb n hx)
      simp only [one_div, Set.mem_iUnion, Metric.mem_ball, exists_prop] at hi
      use i, hi.1
      apply lt_trans hi.2 ?_
      rw [inv_eq_one_div]
      exact hn
    aesop

[Josha Dekker]

Probably this is very easy to resolve, but I'm probably doing something stupid here...

[Felix Weilacher]

You say "lean doesn't know the spaces agree", but you haven't even introduced a metric. Your first have just says that the space is metrizable

[Felix Weilacher]

Try

letI := UniformSpace.pseudoMetricSpace (X := α)
have := Metric.totallyBounded_iff.mp h

[Josha Dekker]

Oh, I see! Thanks, I’ll try it after dinner!

[Josha Dekker]

Thanks, that worked (I forgot about letI)!

[Anatole Dedecker]

Casual reminder than the I in letI changed meaning from Lean 3 to Lean 4 (from "instance" to "inline") and you can also use let and have it picked up by the typeclass system

[Anatole Dedecker]

Also, I think it would really help beginners (and not only them, I’ve lost some time recently due to this…) if we could have a warning when using have on data and suggest using let/set instead.

[Felix Weilacher]

That's a good idea, but I'll point out that it wouldn't have helped here. docs#UniformSpace.pseudoMetrizableSpace is Prop-valued. The fix required switching to docs#UniformSpace.pseudoMetricSpace

[Damiano Testa]

There is a PR with the have/let linter: #12190.