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.

source

class TopologicalSpace.PseudoMetrizableSpace (X : Type u_5) [t : TopologicalSpace 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 : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X.

exists_pseudo_metric : ∃ (m : PseudoMetricSpace X), UniformSpace.toTopologicalSpace = t

Instances

source

instance PseudoMetricSpace.toPseudoMetrizableSpace {X : Type u_5} [m : PseudoMetricSpace X] :

TopologicalSpace.PseudoMetrizableSpace X

Equations

⋯ = ⋯

source

noncomputable def TopologicalSpace.pseudoMetrizableSpacePseudoMetric (X : Type u_5) [TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X] :

PseudoMetricSpace X

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

Equations

TopologicalSpace.pseudoMetrizableSpacePseudoMetric X = PseudoMetricSpace.replaceTopology (Exists.choose ⋯) ⋯

Instances For

source

instance TopologicalSpace.pseudoMetrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace.PseudoMetrizableSpace Y] :

TopologicalSpace.PseudoMetrizableSpace (X × Y)

Equations

⋯ = ⋯

source

theorem Inducing.pseudoMetrizableSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y} (hf : Inducing f) :

TopologicalSpace.PseudoMetrizableSpace X

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

source

instance TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology {X : Type u_2} [TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X] :

FirstCountableTopology X

Every pseudo-metrizable space is first countable.

Equations

⋯ = ⋯

source

instance TopologicalSpace.PseudoMetrizableSpace.subtype {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] (s : Set X) :

TopologicalSpace.PseudoMetrizableSpace ↑s

Equations

⋯ = ⋯

source

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

TopologicalSpace.PseudoMetrizableSpace ((i : ι) → π i)

Equations

⋯ = ⋯

source

class TopologicalSpace.MetrizableSpace (X : Type u_5) [t : TopologicalSpace 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 : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X.