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)
[topological_space X]
[normal_space X]
[topological_space.second_countable_topology 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)
[topological_space X]
[normal_space X]
[topological_space.second_countable_topology 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.