Completely (pseudo)metrizable spaces

A topological space is completely (pseudo)metrizable if one can endow it with a (Pseudo)MetricSpace structure which makes it complete and gives the same topology. This typeclass allows to state theorems which do not require a (Pseudo)MetricSpace structure to make sense without introducing such a structure. It is in particular useful in measure theory, where one often assumes that a space is a PolishSpace, i.e. a separable and completely metrizable space. Sometimes the separability hypothesis is not needed and the right assumption is then IsCompletelyMetrizableSpace.

Main definition

• IsCompletelyPseudoMetrizableSpace X: A topological space is completely pseudometrizable if there exists a pseudometric space structure compatible with the topology which makes the space complete. To endow such a space with a compatible distance, use letI := upgradeIsCompletelyPseudoMetrizable X.

• IsCompletelyMetrizableSpace X: A topological space is completely metrizable if there exists a metric space structure compatible with the topology which makes the space complete. To endow such a space with a compatible distance, use letI := upgradeIsCompletelyMetrizable X.

Implementation note

Given a IsCompletely(Pseudo)MetrizableSpace X instance, one may want to endow X with a complete (pseudo)metric. This can be done by writing letI := upgradeIsCompletely(Pseudo)Metrizable X, which will endow X with an UpgradedIsCompletely(Pseudo)MetrizableSpace X instance. This class is a convenience class and no instance should be registered for it.

class TopologicalSpace.IsCompletelyPseudoMetrizableSpace (X : Type u_3) [t : TopologicalSpace X] : Prop

A topological space is completely pseudometrizable if there exists a pseudometric space structure compatible with the topology which makes the space complete. To endow such a space with a compatible distance, use letI := upgradeIsCompletelyPseudoMetrizable X.

• complete : ∃ (m : PseudoMetricSpace X), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X

@[instance 100]

instance PseudoMetricSpace.toIsCompletelPseudoMetrizableSpace {X : Type u_1} [PseudoMetricSpace X] [CompleteSpace X] : TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

class TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace (X : Type u_3) extends PseudoMetricSpace X, CompleteSpace X : Type u_3

A convenience class, for a completely pseudometrizable space endowed with a complete pseudometric. No instance of this class should be registered: It should be used as letI := upgradeIsCompletelyPseudoMetrizable X to endow a completely pseudometrizable space with a complete pseudometric.

• dist : X → X → ℝ
• dist_self (x : X) : dist x x = 0
• dist_comm (x y : X) : dist x y = dist y x
• dist_triangle (x y z : X) : dist x z ≤ dist x y + dist y z
• edist : X → X → ENNReal
• edist_dist (x y : X) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace X
• uniformity_dist : uniformity X = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : X × X | dist p.1 p.2 < ε}
• toBornology : Bornology X
• cobounded_sets : (Bornology.cobounded X).sets = {s : Set X | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• complete {f : Filter X} : Cauchy f → ∃ (x : X), f ≤ nhds x

@[instance 100]

instance TopologicalSpace.IsCompletelyPseudoMetrizableSpace.of_completeSpace_pseudometrizable {X : Type u_1} [UniformSpace X] [CompleteSpace X] [(uniformity X).IsCountablyGenerated] : IsCompletelyPseudoMetrizableSpace X

noncomputable def TopologicalSpace.completelyPseudoMetrizableMetric (X : Type u_3) [TopologicalSpace X] [h : IsCompletelyPseudoMetrizableSpace X] : PseudoMetricSpace X

Construct on a completely pseudometrizable space a pseudometric (compatible with the topology) which is complete.

Equations

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

theorem TopologicalSpace.complete_completelyPseudoMetrizableMetric (X : Type u_3) [ht : TopologicalSpace X] [h : IsCompletelyPseudoMetrizableSpace X] : CompleteSpace X

noncomputable def TopologicalSpace.upgradeIsCompletelyPseudoMetrizable (X : Type u_3) [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] : UpgradedIsCompletelyPseudoMetrizableSpace X

This definition endows a completely pseudometrizable space with a complete pseudometric. Use it as: letI := upgradeIsCompletelyPseudoMetrizable X.

Equations

• TopologicalSpace.upgradeIsCompletelyPseudoMetrizable X = { toPseudoMetricSpace := TopologicalSpace.completelyPseudoMetrizableMetric X, toCompleteSpace := ⋯ }

@[instance 90]

instance TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] : TopologicalSpace.PseudoMetrizableSpace X

Note: the priority is set to 90 to ensure that this instance is only applied after PseudoEMetricSpace.pseudoMetrizableSpace. This prevents unnecessary attempts to infer completeness.

instance TopologicalSpace.IsCompletelyPseudoMetrizableSpace.pi_countable {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), IsCompletelyPseudoMetrizableSpace (X i)] : IsCompletelyPseudoMetrizableSpace ((i : ι) → X i)

A countable product of completely pseudometrizable spaces is completely pseudometrizable.

instance TopologicalSpace.IsCompletelyPseudoMetrizableSpace.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyPseudoMetrizableSpace Y] : IsCompletelyPseudoMetrizableSpace (X × Y)

The product of two completely pseudometrizable spaces is completely pseudometrizable.

instance TopologicalSpace.IsCompletelyPseudoMetrizableSpace.sum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyPseudoMetrizableSpace Y] : IsCompletelyPseudoMetrizableSpace (X ⊕ Y)

The disjoint union of two completely pseudometrizable spaces is completely pseudometrizable.

theorem Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : TopologicalSpace.IsCompletelyPseudoMetrizableSpace X

Given a closed embedding into a completely pseudometrizable space, the source space is also completely pseudometrizable.

theorem IsClosed.isCompletelyPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] {s : Set X} (hs : IsClosed s) : TopologicalSpace.IsCompletelyPseudoMetrizableSpace ↑s

A closed subset of a completely pseudometrizable space is also completely pseudometrizable.

class TopologicalSpace.IsCompletelyMetrizableSpace (X : Type u_3) [t : TopologicalSpace X] : Prop

A topological space is completely metrizable if there exists a metric space structure compatible with the topology which makes the space complete. To endow such a space with a compatible distance, use letI := upgradeIsCompletelyMetrizable X.

• complete : ∃ (m : MetricSpace X), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X

instance TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : IsCompletelyPseudoMetrizableSpace X

A completely metrizable space is completely pseudometrizable.

theorem TopologicalSpace.IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace {X : Type u_1} [TopologicalSpace X] [IsCompletelyPseudoMetrizableSpace X] [T0Space X] : IsCompletelyMetrizableSpace X

A completely pseudometrizable T0 space is completely metrizable.

@[instance 100]

instance MetricSpace.toIsCompletelyMetrizableSpace {X : Type u_1} [MetricSpace X] [CompleteSpace X] : TopologicalSpace.IsCompletelyMetrizableSpace X

class TopologicalSpace.UpgradedIsCompletelyMetrizableSpace (X : Type u_3) extends MetricSpace X, CompleteSpace X : Type u_3

A convenience class, for a completely metrizable space endowed with a complete metric. No instance of this class should be registered: It should be used as letI := upgradeIsCompletelyMetrizable X to endow a completely metrizable space with a complete metric.

• dist : X → X → ℝ
• dist_self (x : X) : dist x x = 0
• dist_comm (x y : X) : dist x y = dist y x
• dist_triangle (x y z : X) : dist x z ≤ dist x y + dist y z
• edist : X → X → ENNReal
• edist_dist (x y : X) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace X
• uniformity_dist : uniformity X = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : X × X | dist p.1 p.2 < ε}
• toBornology : Bornology X
• cobounded_sets : (Bornology.cobounded X).sets = {s : Set X | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : X} : dist x y = 0 → x = y
• complete {f : Filter X} : Cauchy f → ∃ (x : X), f ≤ nhds x

@[instance 100]

instance TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable {X : Type u_1} [UniformSpace X] [CompleteSpace X] [(uniformity X).IsCountablyGenerated] [T0Space X] : IsCompletelyMetrizableSpace X

noncomputable def TopologicalSpace.completelyMetrizableMetric (X : Type u_3) [TopologicalSpace X] [h : IsCompletelyMetrizableSpace X] : MetricSpace X

Construct on a completely metrizable space a metric (compatible with the topology) which is complete.

Equations

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

theorem TopologicalSpace.complete_completelyMetrizableMetric (X : Type u_3) [ht : TopologicalSpace X] [h : IsCompletelyMetrizableSpace X] : CompleteSpace X

noncomputable def TopologicalSpace.upgradeIsCompletelyMetrizable (X : Type u_3) [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : UpgradedIsCompletelyMetrizableSpace X

This definition endows a completely metrizable space with a complete metric. Use it as: letI := upgradeIsCompletelyMetrizable X.

Equations

• TopologicalSpace.upgradeIsCompletelyMetrizable X = { toMetricSpace := TopologicalSpace.completelyMetrizableMetric X, toCompleteSpace := ⋯ }

@[instance 90]

instance TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace {X : Type u_1} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : TopologicalSpace.MetrizableSpace X

Note: the priority is set to 90 to ensure that this instance is only applied after EMetricSpace.metrizableSpace. This prevents unnecessary attempts to infer completeness.

instance TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), IsCompletelyMetrizableSpace (X i)] : IsCompletelyMetrizableSpace ((i : ι) → X i)

A countable product of completely metrizable spaces is completely metrizable.

instance TopologicalSpace.IsCompletelyMetrizableSpace.sigma {ι : Type u_3} {X : ι → Type u_4} [(n : ι) → TopologicalSpace (X n)] [∀ (n : ι), IsCompletelyMetrizableSpace (X n)] : IsCompletelyMetrizableSpace ((n : ι) × X n)

A disjoint union of completely metrizable spaces is completely metrizable.

instance TopologicalSpace.IsCompletelyMetrizableSpace.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyMetrizableSpace Y] : IsCompletelyMetrizableSpace (X × Y)

The product of two completely metrizable spaces is completely metrizable.

instance TopologicalSpace.IsCompletelyMetrizableSpace.sum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyMetrizableSpace Y] : IsCompletelyMetrizableSpace (X ⊕ Y)

The disjoint union of two completely metrizable spaces is completely metrizable.

theorem Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace.IsCompletelyMetrizableSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : TopologicalSpace.IsCompletelyMetrizableSpace X

Given a closed embedding into a completely metrizable space, the source space is also completely metrizable.

@[instance 50]

instance TopologicalSpace.IsCompletelyMetrizableSpace.discrete {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : IsCompletelyMetrizableSpace X

Any discrete space is completely metrizable.

theorem IsClosed.isCompletelyMetrizableSpace {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X] {s : Set X} (hs : IsClosed s) : TopologicalSpace.IsCompletelyMetrizableSpace ↑s

A closed subset of a completely metrizable space is also completely metrizable.

instance TopologicalSpace.IsCompletelyMetrizableSpace.univ {X : Type u_1} [TopologicalSpace X] [IsCompletelyMetrizableSpace X] : IsCompletelyMetrizableSpace ↑Set.univ