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 let := upgradeIsCompletelyMetrizable α.
• IsClosed.polishSpace: a closed subset of a Polish space is Polish.
• IsGδ.polishSpace: a countable intersection of open subsets 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 α

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

@[deprecated "No replacement" (since := "2026-10-14")]

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_reducible, deprecated "No replacement" (since := "2026-10-14")]

noncomputable 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)ᶜ| }

@[deprecated "No replacement" (since := "2026-10-14")]

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)ᶜ|

@[deprecated "No replacement" (since := "2026-10-14")]

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_reducible, deprecated "No replacement" (since := "2026-10-14")]

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

Equations

• TopologicalSpace.Opens.CompleteCopy.inst = { IsOpen := TopologicalSpace.Opens.CompleteCopy.inst._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

@[deprecated "No replacement" (since := "2026-10-14")]

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

@[deprecated "No replacement" (since := "2026-10-14")]

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

@[instance_reducible, deprecated "No replacement" (since := "2026-10-14")]

noncomputable 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

@[deprecated "No replacement" (since := "2026-10-14")]

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

A Gδ subset of a Polish space is Polish

In particular, an open subset of a Polish space is Polish.

To prove this fact, we follow a proof attributed to A. Bernshteyn. We homeomorphically map a Gδ subset of α to a subset of α × (ℕ → ℝ≥0), which is closed and thus Polish.

noncomputable def GδEmbedding.gδEmbedding {α : Type u_1} [MetricSpace α] {ι : Type u_3} (U : ι → Set α) (x : ↑(⋂ (i : ι), U i)) : α × (ι → NNReal)

The map x ↦ (x, fun i ↦ d(x, U iᶜ)⁻¹) from ⋂ i, U i into α × (ι → ℝ≥0). When the U i are open, this is a closed embedding: the i-th coordinate of the second component blows up as x approaches the boundary of U i, so that the boundary is sent "to infinity". This guarantees limit points will have their first coordinates within all of the U i.

Equations

• GδEmbedding.gδEmbedding U x = (↑x, fun (i : ι) => (Metric.infEDist (↑x) (U i)ᶜ)⁻¹.toNNReal)

theorem GδEmbedding.inv_infEDist_compl_ne_top {α : Type u_1} [MetricSpace α] {ι : Type u_3} {U : ι → Set α} (hUo : ∀ (i : ι), IsOpen (U i)) (x : ↑(⋂ (i : ι), U i)) (i : ι) : (Metric.infEDist (↑x) (U i)ᶜ)⁻¹ ≠ ⊤

theorem GδEmbedding.continuous_gδEmbedding {α : Type u_1} [MetricSpace α] {ι : Type u_3} {U : ι → Set α} (hUo : ∀ (i : ι), IsOpen (U i)) : Continuous (gδEmbedding U)

theorem GδEmbedding.range_gδEmbedding {α : Type u_1} [MetricSpace α] {ι : Type u_3} {U : ι → Set α} (hUo : ∀ (i : ι), IsOpen (U i)) : Set.range (gδEmbedding U) = {q : α × (ι → NNReal) | ∀ (i : ι), (Metric.infEDist q.1 (U i)ᶜ)⁻¹ = ↑(q.2 i)}

This characterization of the range of gδEmbedding as an intersection makes it easy to show that the range is closed.

theorem GδEmbedding.isClosedEmbedding_gδEmbedding {α : Type u_1} [MetricSpace α] {ι : Type u_3} {U : ι → Set α} (hUo : ∀ (i : ι), IsOpen (U i)) : Topology.IsClosedEmbedding (gδEmbedding U)

theorem IsGδ.isCompletelyMetrizableSpace {α : Type u_4} [TopologicalSpace α] [TopologicalSpace.IsCompletelyMetrizableSpace α] {s : Set α} (hs : IsGδ s) : TopologicalSpace.IsCompletelyMetrizableSpace ↑s

A Gδ subset of a completely metrizable space is also completely metrizable.

theorem IsGδ.polishSpace {α : Type u_4} [TopologicalSpace α] [PolishSpace α] {s : Set α} (hs : IsGδ s) : PolishSpace ↑s

A Gδ subset of a Polish space is also Polish.

theorem IsOpen.isCompletelyMetrizableSpace {α : Type u_4} [TopologicalSpace α] [TopologicalSpace.IsCompletelyMetrizableSpace α] {s : Set α} (hs : IsOpen s) : TopologicalSpace.IsCompletelyMetrizableSpace ↑s

An open subset of a completely metrizable space is also completely metrizable.

theorem IsOpen.polishSpace {α : Type u_4} [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)