mathlib documentation

topology.metric_space.metrizable

Metrizability of a regular topological space with second countable topology #

In this file we define metrizable topological spaces, i.e., topological spaces for which there exists a metric space structure that generates the same topology.

We also show that a regular topological space with second countable topology X is metrizable.

First we prove that X can be embedded into l^∞, then use this embedding to pull back the metric space structure.

@[class]
structure topological_space.pseudo_metrizable_space (X : Type u_5) [t : topological_space X] :
Prop

A topological space is pseudo metrizable if there exists a pseudo metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : pseudo_metric_space X := topological_space.pseudo_metrizable_space_pseudo_metric X.

Instances of this typeclass

Given an inducing map of a topological space into a pseudo metrizable space, the source space is also pseudo metrizable.

@[protected, instance]
def topological_space.pseudo_metrizable_space_pi {ι : Type u_1} {π : ι → Type u_4} [fintype ι] [Π (i : ι), topological_space (π i)] [∀ (i : ι), topological_space.pseudo_metrizable_space (π i)] :
@[class]
structure topological_space.metrizable_space (X : Type u_5) [t : topological_space X] :
Prop

A topological space is metrizable if there exists a metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : metric_space X := topological_space.metrizable_space_metric X

Instances of this typeclass
@[protected, instance]

Given an embedding of a topological space into a metrizable space, the source space is also metrizable.

@[protected, instance]
def topological_space.metrizable_space_pi {ι : Type u_1} {π : ι → Type u_4} [fintype ι] [Π (i : ι), topological_space (π i)] [∀ (i : ι), topological_space.metrizable_space (π i)] :

A regular topological space with second countable topology can be embedded into l^∞ = ℕ →ᵇ ℝ.

Urysohn's metrization theorem (Tychonoff's version): a regular topological space with second countable topology X is metrizable, i.e., there exists a metric space structure that generates the same topology.