Theorems · Theorem · general topology

Perfect.splitting

∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [T25Space α],
  Perfect C →
    C.Nonempty → ∃ C₀ C₁, (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.

Defined in

Mathlib.Topology.Perfect

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceT25Space