# 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.

source
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^∞ = ℕ →ᵇ ℝ`.

source
@[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.

source
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^∞ = ℕ →ᵇ ℝ`.

source
@[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.