HepLean Documentation

Mathlib.Topology.Metrizable.Urysohn

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
@[deprecated TopologicalSpace.exists_isInducing_l_infty]
theorem TopologicalSpace.exists_inducing_l_infty (X : Type u_1) [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] :
∃ (f : X → BoundedContinuousFunction ℕ ℝ), Topology.IsInducing f

Alias of TopologicalSpace.exists_isInducing_l_infty.

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] :
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
  • ⋯ = ⋯
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] :
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
  • ⋯ = ⋯
source
@[deprecated TopologicalSpace.metrizableSpace_of_t3_secondCountable]
def TopologicalSpace.metrizableSpace_of_t3_second_countable (X : Type u_1) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] :
TopologicalSpace.MetrizableSpace X

Alias of TopologicalSpace.metrizableSpace_of_t3_secondCountable.

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
Instances For