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.

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

@[instance 100]

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

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 = ⋯.choose.replaceTopology ⋯

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)

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

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

@[deprecated Topology.IsInducing.pseudoMetrizableSpace]

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

Alias of Topology.IsInducing.pseudoMetrizableSpace.

---

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

@[instance 100]

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

Every pseudo-metrizable space is first countable.

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

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

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.

• exists_metric : ∃ (m : MetricSpace X), UniformSpace.toTopologicalSpace = t

@[instance 100]

instance MetricSpace.toMetrizableSpace {X : Type u_5} [m : MetricSpace X] : TopologicalSpace.MetrizableSpace X

@[instance 100]

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

noncomputable def TopologicalSpace.metrizableSpaceMetric (X : Type u_5) [TopologicalSpace X] [h : TopologicalSpace.MetrizableSpace X] : MetricSpace X

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

Equations

• TopologicalSpace.metrizableSpaceMetric X = ⋯.choose.replaceTopology ⋯

@[instance 100]

instance TopologicalSpace.t2Space_of_metrizableSpace {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] : T2Space X

instance TopologicalSpace.metrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace X] [TopologicalSpace.MetrizableSpace Y] : TopologicalSpace.MetrizableSpace (X × Y)

theorem Topology.IsEmbedding.metrizableSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) : TopologicalSpace.MetrizableSpace X

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

@[deprecated Topology.IsEmbedding.metrizableSpace]

theorem Embedding.metrizableSpace {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.MetrizableSpace Y] {f : X → Y} (hf : Topology.IsEmbedding f) : TopologicalSpace.MetrizableSpace X

Alias of Topology.IsEmbedding.metrizableSpace.

---

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} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] (s : Set X) : TopologicalSpace.MetrizableSpace ↑s

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

theorem TopologicalSpace.IsSeparable.secondCountableTopology {X : Type u_2} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X} (hs : TopologicalSpace.IsSeparable s) : SecondCountableTopology ↑s

instance TopologicalSpace.instSecondCountableTopologyOfCompactSpaceOfMetrizableSpace (X : Type u_5) [TopologicalSpace X] [c : CompactSpace X] [TopologicalSpace.MetrizableSpace X] : SecondCountableTopology X