Metrizable Spaces

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 define it without any reference to metric spaces in order to avoid importing the real numbers. For the proof that metrizable spaces admit a compatible metric, see Mathlib/Topology/Metrizable/Uniformity.lean.

class TopologicalSpace.PseudoMetrizableSpace (X : Type u_5) [t : TopologicalSpace X] : Prop

A topological space is pseudometrizable if there exists a pseudometric space structure compatible with the topology. To minimize imports, we implement this class in terms of the existence of a countably generated uniformity inducing the topology, which is mathematically equivalent. To endow such a space with a compatible uniformity, use letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X. To endow such a space with a compatible distance, use letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X.

• exists_countably_generated : ∃ (u : UniformSpace X), u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated

@[instance 100]

instance UniformSpace.pseudoMetrizableSpace {X : Type u_5} [u : UniformSpace X] [hu : (uniformity X).IsCountablyGenerated] : TopologicalSpace.PseudoMetrizableSpace X

A uniform space with countably generated 𝓤 X is pseudometrizable.

@[reducible, inline]

noncomputable abbrev TopologicalSpace.pseudoMetrizableSpaceUniformity (X : Type u_5) [TopologicalSpace X] [h : PseudoMetrizableSpace X] : UniformSpace X

Construct on a pseudometrizable space a countably generated uniformity compatible with the topology. Use pseudoMetrizableSpaceUniformity_countably_generated for a proof that this uniformity is countably generated.

Equations

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

theorem TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated (X : Type u_5) [TopologicalSpace X] [h : PseudoMetrizableSpace X] : (uniformity X).IsCountablyGenerated

The uniformity coming from pseudoMetrizableSpaceUniformity is countably generated..

instance TopologicalSpace.pseudoMetrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [PseudoMetrizableSpace X] [PseudoMetrizableSpace Y] : 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 : IsInducing f) : TopologicalSpace.PseudoMetrizableSpace X

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

@[instance 100]

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

Every pseudo-metrizable space is first countable.

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

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

instance TopologicalSpace.PseudoMetrizableSpace.regularSpace {X : Type u_2} [TopologicalSpace X] [PseudoMetrizableSpace X] : RegularSpace X

class TopologicalSpace.MetrizableSpace (X : Type u_5) [t : TopologicalSpace X] extends TopologicalSpace.PseudoMetrizableSpace X, T0Space X : Prop

A topological space is metrizable if there exists a metric space structure compatible with the topology. To minimize imports, we implement this class in terms of the existence of a countably generated uniformity inducing the topology, which is mathematically equivalent. To endow such a space with a compatible uniformity, use letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X. To endow such a space with a compatible distance, use letI : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X.

• exists_countably_generated : ∃ (u : UniformSpace X), u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated
• t0 ⦃x y : X⦄ : Inseparable x y → x = y

@[instance 100]

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

@[instance 100]

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

instance TopologicalSpace.metrizableSpace_prod {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [MetrizableSpace X] [MetrizableSpace Y] : 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 : IsEmbedding 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] [MetrizableSpace X] (s : Set X) : MetrizableSpace ↑s

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

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

instance TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace (X : Type u_5) [TopologicalSpace X] [LindelofSpace X] [PseudoMetrizableSpace X] : SecondCountableTopology X

theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset {X : Type u_2} [TopologicalSpace X] [PseudoMetrizableSpace X] {s : Set X} (hs : IsSeparable s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

If a set s is separable in a pseudo metrizable space, then it admits a countable dense subset. This is not obvious, as the countable set whose closure covers s given by the definition of separability does not need in general to be contained in s.

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

If a set s is separable, then the corresponding subtype is separable in a pseudo metrizable space. This is not obvious, as the countable set whose closure covers s does not need in general to be contained in s.

@[instance 100]

instance TopologicalSpace.DiscreteTopology.metrizableSpace {X : Type u_2} [TopologicalSpace X] [DiscreteTopology X] : MetrizableSpace X