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
Cis 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.
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,
- [Kec95] (Chapter 6)
accumulation point, perfect set, Cantor-Bendixson.
x is an accumulation point of a set
U is a neighborhood of
x is an accumulation point of
U ∩ C.
C is preperfect if all of its points are accumulation points of itself.
C is nonempty and
α is a T1 space, this is equivalent to the closure of
C being perfect.
- preperfect C = ∀ (x : α), x ∈ C → acc_pt x (filter.principal C)
- closed : is_closed C
- acc : preperfect C
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.
The intersection of a preperfect set and an open set is preperfect
The closure of a preperfect set is perfect.
For a converse, see
In a T1 space, being preperfect is equivalent to having perfect closure.
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.