English
Given a perfect set, one can always find two disjoint perfect subsets contained in it, improving the Cantor-Bendixson decomposition.
Русский
Дано совершенное множество; всегда можно найти две непересекающиеся совершенные подмножества внутри него.
LaTeX
$$$\exists C_0, C_1 \subseteq C \; (\text{Perfect}(C_0) \land \text{Perfect}(C_1) \land C_0 \cap C_1 = \emptyset).$$$
Lean4
/-- 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. -/
theorem splitting [T25Space α] (hC : Perfect C) (hnonempty : C.Nonempty) :
∃ C₀ C₁ : Set α, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C) ∧ Disjoint C₀ C₁ :=
by
obtain ⟨y, yC⟩ := hnonempty
obtain ⟨x, xC, hxy⟩ : ∃ x ∈ C, x ≠ y := by
have := hC.acc _ yC
rw [accPt_iff_nhds] at this
rcases this univ univ_mem with ⟨x, xC, hxy⟩
exact ⟨x, xC.2, hxy⟩
obtain ⟨U, xU, Uop, V, yV, Vop, hUV⟩ := exists_open_nhds_disjoint_closure hxy
use closure (U ∩ C), closure (V ∩ C)
constructor <;> rw [← and_assoc]
· refine ⟨hC.closure_nhds_inter x xC xU Uop, ?_⟩
rw [hC.closed.closure_subset_iff]
exact inter_subset_right
constructor
· refine ⟨hC.closure_nhds_inter y yC yV Vop, ?_⟩
rw [hC.closed.closure_subset_iff]
exact inter_subset_right
apply Disjoint.mono _ _ hUV <;> apply closure_mono <;> exact inter_subset_left
