# mathlibdocumentation

topology.metric_space.metrizable_uniformity

# Metrizable uniform spaces #

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

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) :

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
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) :
= ⨅ (l : list X), (x :: l) (l ++ [y])).sum
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) :
(d x y)
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 *

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.

@[protected]
theorem uniform_space.metrizable_uniformity (X : Type u_1)  :
∃ (I : ,

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.

@[protected]
noncomputable def uniform_space.pseudo_metric_space (X : Type u_1)  :

A pseudo_metric_space instance compatible with a given uniform_space structure.

Equations
@[protected]
noncomputable def uniform_space.metric_space (X : Type u_1) [t0_space X] :

A metric_space instance compatible with a given uniform_space structure.

Equations
@[protected, instance]
def uniform_space.pseudo_metrizable_space {X : Type u_1}  :

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

theorem uniform_space.metrizable_space {X : Type u_1} [t0_space X] :

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