The perfect set theorem and the cardinality of Borel sets

Mathlib proves the perfect set theorem for closed sets: an uncountable closed subset of a Polish space contains the range of a continuous injection of Cantor space (IsClosed.exists_nat_bool_injection_of_not_countable). This file extends it to Borel sets. A Borel set is clopen for a finer Polish topology (MeasurableSet.isClopenable); the closed-set theorem applies there, and a map continuous for the finer topology is continuous for the original one.

For cardinality, Mathlib's Borel isomorphism theorem says that an uncountable standard Borel space is Borel isomorphic to Cantor space (PolishSpace.measurableEquivNatBoolOfNotCountable), and a measurable subset of a standard Borel space is standard Borel (MeasurableSet.standardBorel). Hence an uncountable measurable subset of a standard Borel space, such as an uncountable Borel subset of a Polish space, has exactly 𝔠 points: Borel sets satisfy the continuum hypothesis.

Main results

• MeasurableSet.exists_nat_bool_injection_of_not_countable: an uncountable Borel subset of a Polish space contains the range of a continuous injection of Cantor space.
• MeasurableSet.mk_eq_continuum_of_not_countable: an uncountable measurable subset of a standard Borel space has exactly 𝔠 points.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 13.6 (the perfect set theorem for Borel sets, proved through Theorem 13.1 on finer Polish topologies).

theorem MeasurableSet.exists_nat_bool_injection_of_not_countable {X : Type u} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : MeasurableSet s) (hunc : ¬s.Countable) : ∃ (f : (ℕ → Bool) → X), Set.range f ⊆ s ∧ Continuous f ∧ Function.Injective f

The perfect set theorem for Borel sets (Alexandrov–Hausdorff). An uncountable Borel subset of a Polish space contains the range of a continuous injection of Cantor space.

theorem MeasurableSet.mk_eq_continuum_of_not_countable {X : Type u} [MeasurableSpace X] [StandardBorelSpace X] {s : Set X} (hs : MeasurableSet s) (hunc : ¬s.Countable) : Cardinal.mk ↑s = Cardinal.continuum

Borel sets satisfy the continuum hypothesis. An uncountable measurable subset of a standard Borel space, such as an uncountable Borel subset of a Polish space, has exactly continuum many points.