Perfect Sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_is_closed: 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 #

[Kec95] (Chapters 6-7)

Tags #

accumulation point, perfect set, cantor-bendixson.

source

theorem acc_pt.nhds_inter {α : Type u_1} [topological_space α] {C : set α} {x : α} {U : set α} (h_acc : acc_pt x (filter.principal C)) (hU : U ∈ nhds x) :

acc_pt 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.

source

def preperfect {α : Type u_1} [topological_space α] (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 : α), x ∈ C → acc_pt x (filter.principal C)

source

structure perfect {α : Type u_1} [topological_space α] (C : set α) :

Prop

closed : is_closed C
acc : preperfect C

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.

source

theorem preperfect_iff_nhds {α : Type u_1} [topological_space α] {C : set α} :

preperfect C ↔ ∀ (x : α), x ∈ C → ∀ (U : set α), U ∈ nhds x → (∃ (y : α) (H : y ∈ U ∩ C), y ≠ x)

source

theorem preperfect.open_inter {α : Type u_1} [topological_space α] {C U : set α} (hC : preperfect C) (hU : is_open U) :

preperfect (U ∩ C)

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

source

theorem preperfect.perfect_closure {α : Type u_1} [topological_space α] {C : set α} (hC : preperfect C) :

perfect (closure C)

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

source

theorem preperfect_iff_perfect_closure {α : Type u_1} [topological_space α] {C : set α} [t1_space α] :

preperfect C ↔ perfect (closure C)

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

source

theorem perfect.closure_nhds_inter {α : Type u_1} [topological_space α] {C U : set α} (hC : perfect C) (x : α) (xC : x ∈ C) (xU : x ∈ U) (Uop : is_open U) :

perfect (closure (U ∩ C)) ∧ (closure (U ∩ C)).nonempty

source

theorem perfect.splitting {α : Type u_1} [topological_space α] {C : set α} [t2_5_space α] (hC : perfect C) (hnonempty : C.nonempty) :

∃ (C₀ C₁ : set α), (perfect C₀ ∧ C₀.nonempty ∧ C₀ ⊆ C) ∧ (perfect C₁ ∧ C₁.nonempty ∧ 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

source

theorem exists_countable_union_perfect_of_is_closed {α : Type u_1} [topological_space α] {C : set α} [topological_space.second_countable_topology α] (hclosed : is_closed C) :

∃ (V D : set α), V.countable ∧ 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.

source

theorem exists_perfect_nonempty_of_is_closed_of_not_countable {α : Type u_1} [topological_space α] {C : set α} [topological_space.second_countable_topology α] (hclosed : is_closed C) (hunc : ¬C.countable) :

∃ (D : set α), perfect D ∧ D.nonempty ∧ D ⊆ C

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

source

theorem perfect.small_diam_splitting {α : Type u_1} [metric_space α] {C : set α} (hC : perfect C) {ε : ennreal} (hnonempty : C.nonempty) (ε_pos : 0 < ε) :

∃ (C₀ C₁ : set α), (perfect C₀ ∧ C₀.nonempty ∧ C₀ ⊆ C ∧ emetric.diam C₀ ≤ ε) ∧ (perfect C₁ ∧ C₁.nonempty ∧ 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.

source

theorem perfect.exists_nat_bool_injection {α : Type u_1} [metric_space α] {C : set α} (hC : perfect C) (hnonempty : C.nonempty) [complete_space α] :

∃ (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.

source

theorem is_closed.exists_nat_bool_injection_of_not_countable {α : Type u_1} [topological_space α] [polish_space α] {C : set α} (hC : is_closed C) (hunc : ¬C.countable) :

∃ (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.