mathlib3 documentation

topology.metric_space.metrizable

Metrizability of a T₃ topological space with second countable topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define metrizable topological spaces, i.e., topological spaces for which there exists a metric space structure that generates the same topology.

We also show that 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.

source
@[class]
structure topological_space.pseudo_metrizable_space (X : Type u_5) [t : topological_space X] :
Prop

A topological space is pseudo metrizable if there exists a pseudo metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : pseudo_metric_space X := topological_space.pseudo_metrizable_space_pseudo_metric X.

Instances of this typeclass
source
@[protected, instance]
def pseudo_metric_space.to_pseudo_metrizable_space {X : Type u_1} [m : pseudo_metric_space X] :
topological_space.pseudo_metrizable_space X
source
noncomputable def topological_space.pseudo_metrizable_space_pseudo_metric (X : Type u_1) [topological_space X] [h : topological_space.pseudo_metrizable_space X] :
pseudo_metric_space X

Construct on a metrizable space a metric compatible with the topology.

Equations
source
@[protected, instance]
def topological_space.pseudo_metrizable_space_prod {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] [topological_space.pseudo_metrizable_space X] [topological_space.pseudo_metrizable_space Y] :
topological_space.pseudo_metrizable_space (X × Y)
source
theorem inducing.pseudo_metrizable_space {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] [topological_space.pseudo_metrizable_space Y] {f : X → Y} (hf : inducing f) :
topological_space.pseudo_metrizable_space X

Given an inducing map of a topological space into a pseudo metrizable space, the source space is also pseudo metrizable.

source
@[protected, instance]
def topological_space.pseudo_metrizable_space.first_countable_topology {X : Type u_2} [topological_space X] [h : topological_space.pseudo_metrizable_space X] :
topological_space.first_countable_topology X

Every pseudo-metrizable space is first countable.

source
@[protected, instance]
def topological_space.pseudo_metrizable_space.subtype {X : Type u_2} [topological_space X] [topological_space.pseudo_metrizable_space X] (s : set X) :
topological_space.pseudo_metrizable_space ↥s
source
@[protected, instance]
def topological_space.pseudo_metrizable_space_pi {ι : Type u_1} {π : ι → Type u_4} [finite ι] [Π (i : ι), topological_space (π i)] [∀ (i : ι), topological_space.pseudo_metrizable_space (π i)] :
topological_space.pseudo_metrizable_space (Π (i : ι), π i)
source
@[class]
structure topological_space.metrizable_space (X : Type u_5) [t : topological_space X] :
Prop

A topological space is metrizable if there exists a metric space structure compatible with the topology. To endow such a space with a compatible distance, use letI : metric_space X := topological_space.metrizable_space_metric X

Instances of this typeclass
source
@[protected, instance]
def metric_space.to_metrizable_space {X : Type u_1} [m : metric_space X] :
topological_space.metrizable_space X
source
@[protected, instance]
def topological_space.metrizable_space.to_pseudo_metrizable_space {X : Type u_2} [topological_space X] [h : topological_space.metrizable_space X] :
topological_space.pseudo_metrizable_space X
source
noncomputable def topological_space.metrizable_space_metric (X : Type u_1) [topological_space X] [h : topological_space.metrizable_space X] :
metric_space X

Construct on a metrizable space a metric compatible with the topology.

Equations
source
@[protected, instance]
def topological_space.t2_space_of_metrizable_space {X : Type u_2} [topological_space X] [topological_space.metrizable_space X] :
t2_space X
source
@[protected, instance]
def topological_space.metrizable_space_prod {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] [topological_space.metrizable_space X] [topological_space.metrizable_space Y] :
topological_space.metrizable_space (X × Y)
source
theorem embedding.metrizable_space {X : Type u_2} {Y : Type u_3} [topological_space X] [topological_space Y] [topological_space.metrizable_space Y] {f : X → Y} (hf : embedding f) :
topological_space.metrizable_space X

Given an embedding of a topological space into a metrizable space, the source space is also metrizable.

source
@[protected, instance]
def topological_space.metrizable_space.subtype {X : Type u_2} [topological_space X] [topological_space.metrizable_space X] (s : set X) :
topological_space.metrizable_space ↥s
source
@[protected, instance]
def topological_space.metrizable_space_pi {ι : Type u_1} {π : ι → Type u_4} [finite ι] [Π (i : ι), topological_space (π i)] [∀ (i : ι), topological_space.metrizable_space (π i)] :
topological_space.metrizable_space (Π (i : ι), π i)
source
theorem topological_space.exists_embedding_l_infty (X : Type u_2) [topological_space X] [t3_space X] [topological_space.second_countable_topology X] :
∃ (f : X → bounded_continuous_function ℕ ℝ), embedding f

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

source
theorem topological_space.metrizable_space_of_t3_second_countable (X : Type u_2) [topological_space X] [t3_space X] [topological_space.second_countable_topology X] :
topological_space.metrizable_space 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.

source
@[protected, instance]
def topological_space.ennreal.metrizable_space  :
topological_space.metrizable_space ennreal