mathlib documentation

topology.metric_space.metrizable

Metrizability of a normal topological space with second countable topology #

In this file we show that a normal topological space with second countable topology X is metrizable: there exists a metric space structure that generates the same topology.

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

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

A normal topological space with second countable topology X is metrizable: there exists a metric space structure that generates the same topology. This definition provides a metric_space instance such that the corresponding topological_space X instance is definitionally equal to the original one.

Equations