Perfect Sets

In this file we define properties of Perfect subsets of a metric space, including a version of the Cantor-Bendixson Theorem.

Main Statements

• Perfect.exists_nat_bool_injection: A perfect nonempty set in a complete metric space admits an embedding from the Cantor space.

References

• [kechris1995] (Chapters 6-7)

Tags

accumulation point, perfect set, cantor-bendixson.

theorem Perfect.small_diam_splitting {α : Type u_1} [MetricSpace α] {C : Set α} (hC : Perfect C) {ε : ENNReal} (hnonempty : Set.Nonempty C) (ε_pos : 0 < ε) : ∃ (C₀ : Set α) (C₁ : Set α), (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

A refinement of Perfect.splitting for metric spaces, where we also control the diameter of the new perfect sets.

theorem Perfect.exists_nat_bool_injection {α : Type u_1} [MetricSpace α] {C : Set α} (hC : Perfect C) (hnonempty : Set.Nonempty C) [CompleteSpace α] : ∃ (f : (ℕ → Bool) → α), Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Any nonempty perfect set in a complete metric space admits a continuous injection from the Cantor space, ℕ → Bool.

theorem IsClosed.exists_nat_bool_injection_of_not_countable {α : Type u_1} [TopologicalSpace α] [PolishSpace α] {C : Set α} (hC : IsClosed C) (hunc : ¬Set.Countable C) : ∃ (f : (ℕ → Bool) → α), Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f

Any closed uncountable subset of a Polish space admits a continuous injection from the Cantor space ℕ → Bool.