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.

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

@[instance 90]

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
  • =

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

@[instance 90]

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
  • =