topology.perfect

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

## Tags #

accumulation point, perfect set, cantor-bendixson.

theorem acc_pt.nhds_inter {α : Type u_1} {C : set α} {x : α} {U : set α} (h_acc : ) (hU : U nhds x) :

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} (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
structure perfect {α : Type u_1} (C : set α) :
Prop
• closed :
• acc :

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.

theorem preperfect_iff_nhds {α : Type u_1} {C : set α} :
(x : α), x C (U : set α), U nhds x ( (y : α) (H : y U C), y x)
theorem preperfect.open_inter {α : Type u_1} {C U : set α} (hC : preperfect C) (hU : is_open U) :

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

theorem preperfect.perfect_closure {α : Type u_1} {C : set α} (hC : preperfect 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} {C : set α} [t1_space α] :

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

theorem perfect.closure_nhds_inter {α : Type u_1} {C U : set α} (hC : perfect C) (x : α) (xC : x C) (xU : x U) (Uop : is_open U) :
theorem perfect.splitting {α : Type u_1} {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

theorem exists_countable_union_perfect_of_is_closed {α : Type u_1} {C : set α} (hclosed : is_closed C) :
(V D : set α), V.countable 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_is_closed_of_not_countable {α : Type u_1} {C : set α} (hclosed : is_closed C) (hunc : ¬C.countable) :
(D : set α), D.nonempty D C

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

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 ε) (perfect C₁ C₁.nonempty C₁ 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} [metric_space α] {C : set α} (hC : perfect C) (hnonempty : C.nonempty)  :
(f : ( bool) α), C

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

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

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