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

.

## See also #

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

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`

.

## Equations

- Preperfect C = ∀ x ∈ C, AccPt x (Filter.principal C)

## Instances For

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 : IsClosed C
- acc : Preperfect C

## Instances For

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`

.

- univ_preperfect : Preperfect Set.univ

## Instances

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.

## Equations

- ⋯ = ⋯