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 PseudoMetricSpace.toPseudoMetrizableSpace {X : Type u_5} [m : PseudoMetricSpace X] : TopologicalSpace.PseudoMetrizableSpace X

Equations

• (_ : TopologicalSpace.PseudoMetrizableSpace 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

• One or more equations did not get rendered due to their size.

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

• (_ : TopologicalSpace.PseudoMetrizableSpace (X × Y)) = (_ : TopologicalSpace.PseudoMetrizableSpace (X × Y))

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.

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

Every pseudo-metrizable space is first countable.

Equations

• (_ : FirstCountableTopology X) = (_ : FirstCountableTopology X)

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

Equations

• (_ : TopologicalSpace.PseudoMetrizableSpace ↑s) = (_ : TopologicalSpace.PseudoMetrizableSpace { x : X // x ∈ s })

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

Equations

• (_ : TopologicalSpace.PseudoMetrizableSpace ((i : ι) → π 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 MetricSpace.toMetrizableSpace {X : Type u_5} [m : MetricSpace X] : TopologicalSpace.MetrizableSpace X

Equations

• (_ : TopologicalSpace.MetrizableSpace X) = (_ : TopologicalSpace.MetrizableSpace X)

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

Equations

• (_ : TopologicalSpace.PseudoMetrizableSpace 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

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : T2Space 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)

Equations

• (_ : TopologicalSpace.MetrizableSpace (X × Y)) = (_ : TopologicalSpace.MetrizableSpace (X × Y))

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

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

Equations

• (_ : TopologicalSpace.MetrizableSpace ↑s) = (_ : TopologicalSpace.MetrizableSpace { x : X // x ∈ s })

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

Equations

• (_ : TopologicalSpace.MetrizableSpace ((i : ι) → π 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