Documentation

Mathlib.Topology.Metrizable.Uniformity

Metrizable uniform spaces #

In this file we prove that a uniform space with countably generated uniformity filter is pseudometrizable: there exists a PseudoMetricSpace structure that generates the same uniformity. The proof follows [Sergey Melikhov, Metrizable uniform spaces][melikhov2011].

Main definitions #

Main statements #

Tags #

metrizable space, uniform space

noncomputable def PseudoMetricSpace.ofPreNNDist {X : Type u_1} (d : XXNNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) :

The maximal pseudo metric space structure on X such that dist x y ≤ d x y for all x y, where d : X → X → ℝ≥0 is a function such that d x x = 0 and d x y = d y x for all x, y.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem PseudoMetricSpace.dist_ofPreNNDist {X : Type u_1} (d : XXNNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x : X) (y : X) :
    dist x y = (⨅ (l : List X), List.sum (List.zipWith d (x :: l) (l ++ [y])))
    theorem PseudoMetricSpace.dist_ofPreNNDist_le {X : Type u_1} (d : XXNNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x : X) (y : X) :
    dist x y (d x y)
    theorem PseudoMetricSpace.le_two_mul_dist_ofPreNNDist {X : Type u_1} (d : XXNNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))) (x : X) (y : X) :
    (d x y) 2 * dist x y

    Consider a function d : X → X → ℝ≥0 such that d x x = 0 and d x y = d y x for all x, y. Let dist be the largest pseudometric distance such that dist x y ≤ d x y, see PseudoMetricSpace.ofPreNNDist. Suppose that d satisfies the following triangle-like inequality: d x₁ x₄ ≤ 2 * max (d x₁ x₂, d x₂ x₃, d x₃ x₄). Then d x y ≤ 2 * dist x y for all x, y.

    theorem UniformSpace.metrizable_uniformity (X : Type u_2) [UniformSpace X] [Filter.IsCountablyGenerated (uniformity X)] :
    ∃ (I : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace = inst✝¹

    If X is a uniform space with countably generated uniformity filter, there exists a PseudoMetricSpace structure compatible with the UniformSpace structure. Use UniformSpace.pseudoMetricSpace or UniformSpace.metricSpace instead.

    A MetricSpace instance compatible with a given UniformSpace structure.

    Equations
    Instances For

      A uniform space with countably generated 𝓤 X is pseudo metrizable.

      Equations
      • =

      A T₀ uniform space with countably generated 𝓤 X is metrizable. This is not an instance to avoid loops.