Polish spaces

A topological space is Polish if its topology is second-countable and there exists a compatible complete metric. This is the class of spaces that is well-behaved with respect to measure theory. In this file, we establish the basic properties of Polish spaces.

Main definitions and results

• PolishSpace α is a mixin typeclass on a topological space, requiring that the topology is second-countable and compatible with a complete metric. To endow the space with such a metric, use in a proof letI := upgradeIsCompletelyMetrizable α.
• IsClosed.polishSpace: a closed subset of a Polish space is Polish.
• IsOpen.polishSpace: an open subset of a Polish space is Polish.
• exists_nat_nat_continuous_surjective: any nonempty Polish space is the continuous image of the fundamental Polish space ℕ → ℕ.

A fundamental property of Polish spaces is that one can put finer topologies, still Polish, with additional properties:

• exists_polishSpace_forall_le: on a topological space, consider countably many topologies t n, all Polish and finer than the original topology. Then there exists another Polish topology which is finer than all the t n.
• IsClopenable s is a property of a subset s of a topological space, requiring that there exists a finer topology, which is Polish, for which s becomes open and closed. We show that this property is satisfied for open sets, closed sets, for complements, and for countable unions. Once Borel-measurable sets are defined in later files, it will follow that any Borel-measurable set is clopenable. Once the Lusin-Souslin theorem is proved using analytic sets, we will even show that a set is clopenable if and only if it is Borel-measurable, see isClopenable_iff_measurableSet.

Basic properties of Polish spaces

class PolishSpace (α : Type u_3) [h : TopologicalSpace α] extends SecondCountableTopology α, TopologicalSpace.IsCompletelyMetrizableSpace α : Prop

A Polish space is a topological space with second countable topology, that can be endowed with a metric for which it is complete.

To endow a Polish space with a complete metric space structure, do letI := upgradeIsCompletelyMetrizable α.

• is_open_generated_countable : ∃ (b : Set (Set α)), b.Countable ∧ h = TopologicalSpace.generateFrom b
• complete : ∃ (m : MetricSpace α), PseudoMetricSpace.toUniformSpace.toTopologicalSpace = h ∧ CompleteSpace α

instance instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [TopologicalSpace.IsCompletelyMetrizableSpace α] : PolishSpace α

@[deprecated TopologicalSpace.UpgradedIsCompletelyMetrizableSpace (since := "2025-03-14")]

def UpgradedPolishSpace (X : Type u_3) : Type u_3

Alias of TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.

---

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.

Equations

• UpgradedPolishSpace = TopologicalSpace.UpgradedIsCompletelyMetrizableSpace

@[deprecated TopologicalSpace.completelyMetrizableMetric (since := "2025-03-14")]

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

Alias of TopologicalSpace.completelyMetrizableMetric.

---

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

Equations

• polishSpaceMetric = TopologicalSpace.completelyMetrizableMetric

@[deprecated TopologicalSpace.complete_completelyMetrizableMetric (since := "2025-03-14")]

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

Alias of TopologicalSpace.complete_completelyMetrizableMetric.

@[deprecated TopologicalSpace.upgradeIsCompletelyMetrizable (since := "2025-03-14")]

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

Alias of TopologicalSpace.upgradeIsCompletelyMetrizable.

---

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

Equations

• upgradePolishSpace = TopologicalSpace.upgradeIsCompletelyMetrizable

theorem PolishSpace.exists_nat_nat_continuous_surjective (α : Type u_3) [TopologicalSpace α] [PolishSpace α] [Nonempty α] : ∃ (f : (ℕ → ℕ) → α), Continuous f ∧ Function.Surjective f

Any nonempty Polish space is the continuous image of the fundamental space ℕ → ℕ.

theorem Topology.IsClosedEmbedding.polishSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [PolishSpace β] {f : α → β} (hf : IsClosedEmbedding f) : PolishSpace α

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

theorem Equiv.polishSpace_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] [PolishSpace β] (f : α ≃ β) : PolishSpace α

Pulling back a Polish topology under an equiv gives again a Polish topology.

theorem IsClosed.polishSpace {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) : PolishSpace ↑s

A closed subset of a Polish space is also Polish.

theorem CompletePseudometrizable.iInf {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ι → TopologicalSpace α} (ht₀ : ∃ (t₀ : TopologicalSpace α), T2Space α ∧ ∀ (i : ι), t i ≤ t₀) (ht : ∀ (i : ι), ∃ (u : UniformSpace α), CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = t i) : ∃ (u : UniformSpace α), CompleteSpace α ∧ (uniformity α).IsCountablyGenerated ∧ u.toTopologicalSpace = ⨅ (i : ι), t i

theorem PolishSpace.iInf {α : Type u_1} {ι : Type u_3} [Countable ι] {t : ι → TopologicalSpace α} (ht₀ : ∃ (i₀ : ι), ∀ (i : ι), t i ≤ t i₀) (ht : ∀ (i : ι), PolishSpace α) : PolishSpace α

theorem PolishSpace.exists_polishSpace_forall_le {α : Type u_1} {ι : Type u_3} [Countable ι] [t : TopologicalSpace α] [p : PolishSpace α] (m : ι → TopologicalSpace α) (hm : ∀ (n : ι), m n ≤ t) (h'm : ∀ (n : ι), PolishSpace α) : ∃ (t' : TopologicalSpace α), (∀ (n : ι), t' ≤ m n) ∧ t' ≤ t ∧ PolishSpace α

Given a Polish space, and countably many finer Polish topologies, there exists another Polish topology which is finer than all of them.

instance PolishSpace.instENNReal : PolishSpace ENNReal

An open subset of a Polish space is Polish

To prove this fact, one needs to construct another metric, giving rise to the same topology, for which the open subset is complete. This is not obvious, as for instance (0,1) ⊆ ℝ is not complete for the usual metric of ℝ: one should build a new metric that blows up close to the boundary.

def TopologicalSpace.Opens.CompleteCopy {α : Type u_3} [MetricSpace α] (s : Opens α) : Type u_3

A type synonym for a subset s of a metric space, on which we will construct another metric for which it will be complete.

Equations

• s.CompleteCopy = ↥s

instance TopologicalSpace.Opens.CompleteCopy.instDist {α : Type u_1} [MetricSpace α] {s : Opens α} : Dist s.CompleteCopy

A distance on an open subset s of a metric space, designed to make it complete. It is given by dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|, where the second term blows up close to the boundary to ensure that Cauchy sequences for dist' remain well inside s.

Equations

• TopologicalSpace.Opens.CompleteCopy.instDist = { dist := fun (x y : s.CompleteCopy) => dist ↑x ↑y + |1 / Metric.infDist (↑x) (↑s)ᶜ - 1 / Metric.infDist (↑y) (↑s)ᶜ| }

theorem TopologicalSpace.Opens.CompleteCopy.dist_eq {α : Type u_1} [MetricSpace α] {s : Opens α} (x y : s.CompleteCopy) : dist x y = dist ↑x ↑y + |1 / Metric.infDist (↑x) (↑s)ᶜ - 1 / Metric.infDist (↑y) (↑s)ᶜ|

theorem TopologicalSpace.Opens.CompleteCopy.dist_val_le_dist {α : Type u_1} [MetricSpace α] {s : Opens α} (x y : s.CompleteCopy) : dist ↑x ↑y ≤ dist x y

instance TopologicalSpace.Opens.CompleteCopy.inst {α : Type u_1} [MetricSpace α] {s : Opens α} : TopologicalSpace s.CompleteCopy

Equations

• TopologicalSpace.Opens.CompleteCopy.inst = inferInstanceAs (TopologicalSpace ↥s)

instance TopologicalSpace.Opens.CompleteCopy.instSecondCountableTopology {α : Type u_1} [MetricSpace α] {s : Opens α} [SecondCountableTopology α] : SecondCountableTopology s.CompleteCopy

instance TopologicalSpace.Opens.CompleteCopy.instT0Space {α : Type u_1} [MetricSpace α] {s : Opens α} : T0Space s.CompleteCopy

instance TopologicalSpace.Opens.CompleteCopy.instMetricSpace {α : Type u_1} [MetricSpace α] {s : Opens α} : MetricSpace s.CompleteCopy

A metric space structure on a subset s of a metric space, designed to make it complete if s is open. It is given by dist' x y = dist x y + |1 / dist x sᶜ - 1 / dist y sᶜ|, where the second term blows up close to the boundary to ensure that Cauchy sequences for dist' remain well inside s.

This definition ensures the TopologicalSpace structure on TopologicalSpace.Opens.CompleteCopy s is definitionally equal to the original one.

Equations

• TopologicalSpace.Opens.CompleteCopy.instMetricSpace = MetricSpace.ofT0PseudoMetricSpace s.CompleteCopy

instance TopologicalSpace.Opens.CompleteCopy.instCompleteSpace {α : Type u_1} [MetricSpace α] {s : Opens α} [CompleteSpace α] : CompleteSpace s.CompleteCopy

theorem IsOpen.polishSpace {α : Type u_3} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsOpen s) : PolishSpace ↑s

An open subset of a Polish space is also Polish.

Clopenable sets in Polish spaces

def PolishSpace.IsClopenable {α : Type u_1} [t : TopologicalSpace α] (s : Set α) : Prop

A set in a topological space is clopenable if there exists a finer Polish topology for which this set is open and closed. It turns out that this notion is equivalent to being Borel-measurable, but this is nontrivial (see isClopenable_iff_measurableSet).

Equations

• PolishSpace.IsClopenable s = ∃ t' ≤ t, PolishSpace α ∧ IsClosed s ∧ IsOpen s

theorem IsClosed.isClopenable {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsClosed s) : PolishSpace.IsClopenable s

Given a closed set s in a Polish space, one can construct a finer Polish topology for which s is both open and closed.

theorem PolishSpace.IsClopenable.compl {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsClopenable s) : IsClopenable sᶜ

theorem IsOpen.isClopenable {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsOpen s) : PolishSpace.IsClopenable s

theorem PolishSpace.IsClopenable.iUnion {α : Type u_1} [t : TopologicalSpace α] [PolishSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), IsClopenable (s n)) : IsClopenable (⋃ (n : ℕ), s n)