Metrizable uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

pseudo_metric_space.of_prenndist: given a function d : X → X → ℝ≥0 such that d x x = 0 and d x y = d y x for all x y : X, constructs the maximal pseudo metric space structure such that nndist x y ≤ d x y for all x y : X.
uniform_space.pseudo_metric_space: given a uniform space X with countably generated 𝓤 X, constructs a pseudo_metric_space X instance that is compatible with the uniform space structure.
uniform_space.metric_space: given a T₀ uniform space X with countably generated 𝓤 X, constructs a metric_space X instance that is compatible with the uniform space structure.

Main statements #

uniform_space.metrizable_uniformity: if X is a uniform space with countably generated 𝓤 X, then there exists a pseudo_metric_space structure that is compatible with this uniform_space structure. Use uniform_space.pseudo_metric_space or uniform_space.metric_space instead.
uniform_space.pseudo_metrizable_space: a uniform space with countably generated 𝓤 X is pseudo metrizable.
uniform_space.metrizable_space: a T₀ uniform space with countably generated 𝓤 X is metrizable. This is not an instance to avoid loops.

Tags #

metrizable space, uniform space

source

noncomputable def pseudo_metric_space.of_prenndist {X : Type u_1} (d : X → X → nnreal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) :

pseudo_metric_space 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

pseudo_metric_space.of_prenndist d dist_self dist_comm = {to_has_dist := {dist := λ (x y : X), ↑⨅ (l : list X), (list.zip_with d (x :: l) (l ++ [y])).sum}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : X), ↑⟨(λ (x y : X), ↑⨅ (l : list X), (list.zip_with d (x :: l) (l ++ [y])).sum) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : X), ↑⨅ (l : list X), (list.zip_with d (x :: l) (l ++ [y])).sum) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : X), ↑⨅ (l : list X), (list.zip_with d (x :: l) (l ++ [y])).sum) _ _ _, cobounded_sets := _}

source

theorem pseudo_metric_space.dist_of_prenndist {X : Type u_1} (d : X → X → nnreal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x y : X) :

has_dist.dist x y = ↑⨅ (l : list X), (list.zip_with d (x :: l) (l ++ [y])).sum

source

theorem pseudo_metric_space.dist_of_prenndist_le {X : Type u_1} (d : X → X → nnreal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x) (x y : X) :

has_dist.dist x y ≤ ↑(d x y)

source

theorem pseudo_metric_space.le_two_mul_dist_of_prenndist {X : Type u_1} (d : X → X → nnreal) (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 * linear_order.max (d x₁ x₂) (linear_order.max (d x₂ x₃) (d x₃ x₄))) (x y : X) :

↑(d x y) ≤ 2 * has_dist.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 pseudo_metric_space.of_prenndist. 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.

source

@[protected]

theorem uniform_space.metrizable_uniformity (X : Type u_1) [uniform_space X] [(uniformity X).is_countably_generated] :

∃ (I : pseudo_metric_space X), pseudo_metric_space.to_uniform_space = _inst_1

If X is a uniform space with countably generated uniformity filter, there exists a pseudo_metric_space structure compatible with the uniform_space structure. Use uniform_space.pseudo_metric_space or uniform_space.metric_space instead.

source

@[protected]

noncomputable def uniform_space.pseudo_metric_space (X : Type u_1) [uniform_space X] [(uniformity X).is_countably_generated] :

pseudo_metric_space X

A pseudo_metric_space instance compatible with a given uniform_space structure.

Equations

uniform_space.pseudo_metric_space X = _.some.replace_uniformity _

source

@[protected]

noncomputable def uniform_space.metric_space (X : Type u_1) [uniform_space X] [(uniformity X).is_countably_generated] [t0_space X] :

metric_space X

A metric_space instance compatible with a given uniform_space structure.

Equations

uniform_space.metric_space X = metric_space.of_t0_pseudo_metric_space X

source

@[protected, instance]

def uniform_space.pseudo_metrizable_space {X : Type u_1} [uniform_space X] [(uniformity X).is_countably_generated] :

topological_space.pseudo_metrizable_space X

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

source

theorem uniform_space.metrizable_space {X : Type u_1} [uniform_space X] [(uniformity X).is_countably_generated] [t0_space X] :

topological_space.metrizable_space X

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