Urysohn's Metrization Theorem

In this file we prove Urysohn's Metrization Theorem: a T₃ 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.

Implementation notes

We use ℕ →ᵇ ℝ, not lpSpace for l^∞ to avoid heavy imports.

theorem TopologicalSpace.exists_isInducing_l_infty (X : Type u_1) [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : ∃ (f : X → BoundedContinuousFunction ℕ ℝ), Topology.IsInducing f

For a regular topological space with second countable topology, there exists an inducing map to l^∞ = ℕ →ᵇ ℝ.

@[instance 90]

instance TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology (X : Type u_1) [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : PseudoMetrizableSpace X

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

theorem TopologicalSpace.exists_embedding_l_infty (X : Type u_1) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] : ∃ (f : X → BoundedContinuousFunction ℕ ℝ), Topology.IsEmbedding f

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

@[instance 90]

instance TopologicalSpace.metrizableSpace_of_t3_secondCountable (X : Type u_1) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] : MetrizableSpace X

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