Completely metrizable spaces

A topological space is completely metrizable if one can endow it mith a MetricSpace structure which makes it complete and gives the same topology. This typeclass allows to state theorems which do not require a 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

• 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 IsCompletelyMetrizableSpace X instance, one may want to endow X with a complete metric. This can be done by writing letI := upgradeIsCompletelyMetrizable X, which will endow X with an UpgradedIsCompletelyMetrizableSpace X instance. This class is a convenience class and no instance should be registered for it.

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), UniformSpace.toTopologicalSpace = t ∧ CompleteSpace X

@[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 = TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.mk

@[instance 100]

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

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