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

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

- [kechris1995] (Chapters 6-7)

## Tags #

accumulation point, perfect set, cantor-bendixson.

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`

.

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`

.

## Instances For

- closed : IsClosed 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.

## Instances For

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

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.

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.

A refinement of `Perfect.splitting`

for metric spaces, where we also control
the diameter of the new perfect sets.

Any nonempty perfect set in a complete metric space admits a continuous injection
from the Cantor space, `ℕ → Bool`

.

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

.