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_inducing_l_infty (X : Type u_1) [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : ∃ (f : X → BoundedContinuousFunction ℕ ℝ), Inducing f

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

instance TopologicalSpace.PseudoMetrizableSpace.of_regularSpace_secondCountableTopology (X : Type u_1) [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : TopologicalSpace.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.

Equations

• (_ : TopologicalSpace.PseudoMetrizableSpace X) = (_ : TopologicalSpace.PseudoMetrizableSpace X)

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

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

instance TopologicalSpace.metrizableSpace_of_t3_second_countable (X : Type u_1) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] : TopologicalSpace.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.

Equations

• (_ : TopologicalSpace.MetrizableSpace X) = (_ : TopologicalSpace.MetrizableSpace X)