# mathlibdocumentation

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.

theorem topological_space.exists_embedding_l_infty (X : Type u_1) [normal_space X]  :
∃ (f : X → →ᵇ ),

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

noncomputable def topological_space.to_metric_space (X : Type u_1) [normal_space X]  :

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