Perfect Sets

In this file we define perfect subsets of a topological space, and prove some basic properties, including a version of the Cantor-Bendixson Theorem.

Main Definitions

• Perfect C: A set C is perfect, meaning it is closed and every point of it is an accumulation point of itself.

Main Statements

• Perfect.splitting: A perfect nonempty set contains two disjoint perfect nonempty subsets. The main inductive step in the construction of an embedding from the Cantor space to a perfect nonempty complete metric space.
• exists_countable_union_perfect_of_isClosed: One version of the Cantor-Bendixson Theorem: A closed set in a second countable space can be written as the union of a countable set and a perfect set.
• Perfect.exists_nat_bool_injection: A perfect nonempty set in a complete metric space admits an embedding from the Cantor space.

Implementation Notes

We do not require perfect sets to be nonempty.

We define a nonstandard predicate, Preperfect, which drops the closed-ness requirement from the definition of perfect. In T1 spaces, this is equivalent to having a perfect closure, see preperfect_iff_perfect_closure.

References

• [kechris1995] (Chapters 6-7)

Tags

accumulation point, perfect set, cantor-bendixson.

theorem AccPt.nhds_inter {α : Type u_1} [TopologicalSpace α] {C : Set α} {x : α} {U : Set α} (h_acc : AccPt x (Filter.principal C)) (hU : U ∈ nhds x) : AccPt x (Filter.principal (U ∩ C))

If x is an accumulation point of a set C and U is a neighborhood of x, then x is an accumulation point of U ∩ C.

def Preperfect {α : Type u_1} [TopologicalSpace α] (C : Set α) : Prop

A set C is preperfect if all of its points are accumulation points of itself. If C is nonempty and α is a T1 space, this is equivalent to the closure of C being perfect. See preperfect_iff_perfect_closure.

Equations

• Preperfect C = ∀ x ∈ C, AccPt x (Filter.principal C)

structure Perfect {α : Type u_1} [TopologicalSpace α] (C : Set α) : Prop

A set C is called perfect if it is closed and all of its points are accumulation points of itself. Note that we do not require C to be nonempty.

• closed : IsClosed C
• acc : Preperfect C

theorem preperfect_iff_nhds {α : Type u_1} [TopologicalSpace α] {C : Set α} : Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x

theorem Preperfect.open_inter {α : Type u_1} [TopologicalSpace α] {C : Set α} {U : Set α} (hC : Preperfect C) (hU : IsOpen U) : Preperfect (U ∩ C)

The intersection of a preperfect set and an open set is preperfect.

theorem Preperfect.perfect_closure {α : Type u_1} [TopologicalSpace α] {C : Set α} (hC : Preperfect C) : Perfect (closure C)

The closure of a preperfect set is perfect. For a converse, see preperfect_iff_perfect_closure.

theorem preperfect_iff_perfect_closure {α : Type u_1} [TopologicalSpace α] {C : Set α} [T1Space α] : Preperfect C ↔ Perfect (closure C)

In a T1 space, being preperfect is equivalent to having perfect closure.

theorem Perfect.closure_nhds_inter {α : Type u_1} [TopologicalSpace α] {C : Set α} {U : Set α} (hC : Perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U) (Uop : IsOpen U) : Perfect (closure (U ∩ C)) ∧ Set.Nonempty (closure (U ∩ C))

theorem Perfect.splitting {α : Type u_1} [TopologicalSpace α] {C : Set α} [T25Space α] (hC : Perfect C) (hnonempty : Set.Nonempty C) : ∃ (C₀ : Set α) (C₁ : Set α), (Perfect C₀ ∧ Set.Nonempty C₀ ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ Set.Nonempty C₁ ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁

Given a perfect nonempty set in a T2.5 space, we can find two disjoint perfect subsets. This is the main inductive step in the proof of the Cantor-Bendixson Theorem.

theorem exists_countable_union_perfect_of_isClosed {α : Type u_1} [TopologicalSpace α] {C : Set α} [SecondCountableTopology α] (hclosed : IsClosed C) : ∃ (V : Set α) (D : Set α), Set.Countable V ∧ Perfect D ∧ C = V ∪ D

The Cantor-Bendixson Theorem: Any closed subset of a second countable space can be written as the union of a countable set and a perfect set.

theorem exists_perfect_nonempty_of_isClosed_of_not_countable {α : Type u_1} [TopologicalSpace α] {C : Set α} [SecondCountableTopology α] (hclosed : IsClosed C) (hunc : ¬Set.Countable C) : ∃ (D : Set α), Perfect D ∧ Set.Nonempty D ∧ D ⊆ C

Any uncountable closed set in a second countable space contains a nonempty perfect subset.

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.