Perfect sets in metric spaces

A Polish space has at most continuum many points (TauCeti.mk_le_continuum_of_secondCountableTopology). A nonempty perfect subset of a completely metrizable space contains a copy of Cantor space, so it has at least continuum many points. Together these give the cardinality of a nonempty perfect subset of a Polish space: exactly 𝔠.

In a perfect extended metric space, a nonempty open set also splits into two disjoint nonempty open sets of small diameter whose closures stay inside it: the open-set counterpart of Mathlib's Perfect.small_diam_splitting, used to build Cantor schemes of open sets.

The same split holds for an open set with uncountable image under a continuous map f from a second countable extended pseudometric space into a Hausdorff space, with uncountable and disjoint images: the points with a neighbourhood of countable image have countable image by second countability, so the open set contains two condensation points of f with distinct values. This is the step of the perfect set theorem for analytic sets.

Main results

• Perfect.continuum_le_mk: a nonempty perfect subset of a completely metrizable space has at least 𝔠 points.
• Perfect.mk_eq_continuum: a nonempty perfect subset of a Polish space has exactly 𝔠 points.
• IsOpen.exists_disjoint_closure_subset: in a perfect extended metric space, a nonempty open set contains two disjoint nonempty open sets of small diameter, with closures inside it.
• Continuous.exists_split_of_not_countable_image: for a continuous map from a second countable extended pseudometric space into a Hausdorff space, an open set with uncountable image contains two open sets of small diameter, with closures inside it, with uncountable and disjoint images.

References

• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer, 1995, Theorem 6.2 and Corollary 6.3.

theorem Perfect.continuum_le_mk {X : Type u} [TopologicalSpace X] {C : Set X} [TopologicalSpace.IsCompletelyMetrizableSpace X] (hC : Perfect C) (hne : C.Nonempty) : Cardinal.continuum ≤ Cardinal.mk ↑C

A nonempty perfect set in a completely metrizable space has at least continuum many points: it contains the range of a continuous injection of Cantor space.

theorem Perfect.mk_eq_continuum {X : Type u} [TopologicalSpace X] {C : Set X} [PolishSpace X] (hC : Perfect C) (hne : C.Nonempty) : Cardinal.mk ↑C = Cardinal.continuum

A nonempty perfect set in a Polish space has cardinality continuum.

theorem IsOpen.exists_disjoint_closure_subset {X : Type u_1} [EMetricSpace X] [PerfectSpace X] {V : Set X} (hV : IsOpen V) (hne : V.Nonempty) {ε : ENNReal} (hε : 0 < ε) : ∃ (W : Bool → Set X), (∀ (b : Bool), IsOpen (W b)) ∧ (∀ (b : Bool), (W b).Nonempty) ∧ (∀ (b : Bool), closure (W b) ⊆ V) ∧ (∀ (b : Bool), Metric.ediam (W b) ≤ ε) ∧ Disjoint (W false) (W true)

Splitting a nonempty open set in a perfect extended metric space: a nonempty open set V contains two disjoint nonempty open sets of diameter at most ε, with closures inside V.

theorem Continuous.exists_split_of_not_countable_image {X : Type u} [TopologicalSpace X] {Y : Type u_1} [PseudoEMetricSpace Y] [SecondCountableTopology Y] [T2Space X] {f : Y → X} (hf : Continuous f) {U : Set Y} (hU : IsOpen U) (hfU : ¬(f '' U).Countable) {ε : ENNReal} (hε : 0 < ε) : ∃ (W : Bool → Set Y), (∀ (b : Bool), IsOpen (W b) ∧ ¬(f '' W b).Countable ∧ closure (W b) ⊆ U ∧ Metric.ediam (W b) ≤ ε) ∧ ∀ x ∈ W false, ∀ y ∈ W true, f x ≠ f y

Splitting an open set with uncountable image: an open set U with uncountable image under a continuous map f from a second countable extended pseudometric space into a Hausdorff space contains two open sets of diameter at most ε, with closures inside U, with uncountable images under f, and whose images under f are disjoint.