The perfect set theorem for analytic sets

Souslin's perfect set theorem says that an uncountable analytic subset of a Hausdorff space contains the range of a continuous injection of Cantor space. Consequently an analytic set is countable or has exactly continuum many points.

An analytic set is the range of a continuous map f on a Polish space, so the theorem follows from a statement about such maps: if f has uncountable range, then there is a continuous map g of Cantor space into the domain with f ∘ g injective. In the vocabulary of antichains, the kernel Setoid.ker f (the relation f x = f y) has a Cantor antichain.

The proof is a Cantor scheme of open sets with uncountable images. Call a point of the domain a condensation point of f when every neighbourhood of it has uncountable image. By second countability the non-condensation points have countable image, so an open set U with uncountable image contains two condensation points with distinct values. The two values have disjoint neighbourhoods in the Hausdorff target; shrinking around the two points gives two open sets of small diameter, with closures inside U, with uncountable images, and whose images are disjoint (Continuous.exists_split_of_not_countable_image). Iterating this split produces a closure-antitone scheme of vanishing diameter in a complete metric on the domain, and CantorScheme.VanishingDiam.hasCantorAntichainOn turns it into a Cantor antichain of Setoid.ker f.

Main results

• Setoid.hasCantorAntichainOn_ker_univ_of_not_countable_range: a continuous map from a Polish space to a Hausdorff space with uncountable range has a Cantor antichain for its kernel.
• MeasureTheory.AnalyticSet.exists_nat_bool_injection_of_not_countable: the perfect set theorem for analytic sets.
• MeasureTheory.AnalyticSet.mk_eq_continuum_of_not_countable: an uncountable analytic subset of a Hausdorff space has exactly 𝔠 points; the upper bound is MeasureTheory.AnalyticSet.mk_le_continuum.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 29.1 (the perfect set theorem for analytic sets, by a Cantor scheme on the condensation points of a parametrization).
• The scheme is assembled as in Mathlib's Perfect.exists_nat_bool_injection.

theorem Setoid.hasCantorAntichainOn_ker_univ_of_not_countable_range {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [PolishSpace Y] [T2Space X] {f : Y → X} (hf : Continuous f) (hrange : ¬(Set.range f).Countable) : (ker f).HasCantorAntichainOn Set.univ

Cantor antichains for the kernel of a continuous map. A continuous map from a Polish space to a Hausdorff space with uncountable range has a Cantor antichain for its kernel: a continuous map g of Cantor space into the domain with f ∘ g injective.

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

The perfect set theorem for analytic sets (Souslin). An uncountable analytic subset of a Hausdorff space contains the range of a continuous injection of Cantor space.

theorem MeasureTheory.AnalyticSet.mk_eq_continuum_of_not_countable {X : Type u} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : AnalyticSet s) (hunc : ¬s.Countable) : Cardinal.mk ↑s = Cardinal.continuum

Analytic sets satisfy the continuum hypothesis. An uncountable analytic subset of a Hausdorff space has exactly continuum many points.