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

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.

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 : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X.

• exists_pseudo_metric : ∃ (m : ), UniformSpace.toTopologicalSpace = t
Instances
theorem TopologicalSpace.PseudoMetrizableSpace.exists_pseudo_metric {X : Type u_5} [t : ] [self : ] :
∃ (m : ), UniformSpace.toTopologicalSpace = t
@[instance 100]
Equations
• =

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

Equations
• = .choose.replaceTopology
Instances For
instance TopologicalSpace.pseudoMetrizableSpace_prod {X : Type u_2} {Y : Type u_3} [] [] :
Equations
• =
theorem Inducing.pseudoMetrizableSpace {X : Type u_2} {Y : Type u_3} [] [] {f : XY} (hf : ) :

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

@[instance 100]

Every pseudo-metrizable space is first countable.

Equations
• =
Equations
• =
instance TopologicalSpace.pseudoMetrizableSpace_pi {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), ] :
Equations
• =

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 : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X.

• exists_metric : ∃ (m : ), UniformSpace.toTopologicalSpace = t
Instances
theorem TopologicalSpace.MetrizableSpace.exists_metric {X : Type u_5} [t : ] [self : ] :
∃ (m : ), UniformSpace.toTopologicalSpace = t
@[instance 100]
instance MetricSpace.toMetrizableSpace {X : Type u_5} [m : ] :
Equations
• =
@[instance 100]
Equations
• =
noncomputable def TopologicalSpace.metrizableSpaceMetric (X : Type u_5) [] :

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

Equations
• = .choose.replaceTopology
Instances For
@[instance 100]
Equations
• =
instance TopologicalSpace.metrizableSpace_prod {X : Type u_2} {Y : Type u_3} [] [] :
Equations
• =
theorem Embedding.metrizableSpace {X : Type u_2} {Y : Type u_3} [] [] {f : XY} (hf : ) :

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

instance TopologicalSpace.MetrizableSpace.subtype {X : Type u_2} [] (s : Set X) :
Equations
• =
instance TopologicalSpace.metrizableSpace_pi {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), ] :
Equations
• =