# 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.
• PerfectSpace X: A topological space X is perfect if its universe is a perfect set.

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

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

Mathlib.Topology.MetricSpace.Perfect, for properties of perfect sets in metric spaces, namely Polish spaces.

## References #

• [kechris1995] (Chapters 6-7)

## Tags #

accumulation point, perfect set, cantor-bendixson.

theorem AccPt.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 α) :

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
• = xC,
Instances For
theorem perfect_def {α : Type u_1} [] (C : Set α) :
structure Perfect {α : Type u_1} [] (C : Set α) :

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 :
• acc :
Instances For
theorem Perfect.closed {α : Type u_1} [] {C : Set α} (self : ) :
theorem Perfect.acc {α : Type u_1} [] {C : Set α} (self : ) :
theorem preperfect_iff_nhds {α : Type u_1} [] {C : Set α} :
xC, Unhds x, yU C, y x
theorem perfectSpace_def (α : Type u_1) [] :
Preperfect Set.univ
class PerfectSpace (α : Type u_1) [] :

A topological space X is said to be perfect if its universe is a perfect set. Equivalently, this means that 𝓝[≠] x ≠ ⊥ for every point x : X.

Instances
theorem PerfectSpace.univ_preperfect {α : Type u_1} [] [self : ] :
Preperfect Set.univ
theorem PerfectSpace.univ_perfect (α : Type u_1) [] [] :
Perfect Set.univ
theorem Preperfect.open_inter {α : Type u_1} [] {C : Set α} {U : Set α} (hC : ) (hU : ) :

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

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

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 α} [] :

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

theorem Perfect.closure_nhds_inter {α : Type u_1} [] {C : Set α} {U : Set α} (hC : ) (x : α) (xC : x C) (xU : x U) (Uop : ) :
Perfect (closure (U C)) (closure (U C)).Nonempty
theorem Perfect.splitting {α : Type u_1} [] {C : Set α} [] (hC : ) (hnonempty : C.Nonempty) :
∃ (C₀ : Set α) (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_isClosed {α : Type u_1} [] {C : Set α} (hclosed : ) :
∃ (V : Set α) (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_isClosed_of_not_countable {α : Type u_1} [] {C : Set α} (hclosed : ) (hunc : ¬C.Countable) :
∃ (D : Set α), D.Nonempty D C

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

theorem perfectSpace_iff_forall_not_isolated {X : Type u_1} [] :
∀ (x : X), (nhdsWithin x {x}).NeBot
instance PerfectSpace.not_isolated {X : Type u_1} [] [] (x : X) :
(nhdsWithin x {x}).NeBot
Equations
• =