mathlib documentation


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 #

Main Statements #

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 #

Tags #

accumulation point, perfect set, Cantor-Bendixson.

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) :

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} [topological_space α] (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.

structure perfect {α : Type u_1} [topological_space α] (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.

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

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

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

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) :
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

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.

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