English
A variant of the previous nontrivial preperfect lemma under IsPreconnected assumptions.
Русский
Вариант предыдущей леммы о предперфектности при предположении IsPreconnected.
LaTeX
$$$[T1Space α] \; {U : Set α} \; (hu : U.Nontrivial) \; (h : IsPreconnected U) \Rightarrow \text{Preperfect } U.$$$
Lean4
/-- 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. -/
theorem exists_countable_union_perfect_of_isClosed [SecondCountableTopology α] (hclosed : IsClosed C) :
∃ V D : Set α, V.Countable ∧ Perfect D ∧ C = V ∪ D :=
by
obtain ⟨b, bct, _, bbasis⟩ := TopologicalSpace.exists_countable_basis α
let v := {U ∈ b | (U ∩ C).Countable}
let V := ⋃ U ∈ v, U
let D := C \ V
have Vct : (V ∩ C).Countable := by
simp only [V, iUnion_inter]
apply Countable.biUnion
· exact Countable.mono inter_subset_left bct
· exact inter_subset_right
refine ⟨V ∩ C, D, Vct, ⟨?_, ?_⟩, ?_⟩
· refine hclosed.sdiff (isOpen_biUnion fun _ ↦ ?_)
exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub
· rw [preperfect_iff_nhds]
intro x xD E xE
have : ¬(E ∩ D).Countable := by
intro h
obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E := (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE
have hU_cnt : (U ∩ C).Countable := by
apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
· rintro y ⟨yU, yC⟩
by_cases h : y ∈ V
· exact mem_union_right _ (mem_inter h yC)
· exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
exact Countable.union h Vct
have : U ∈ v := ⟨hUb, hU_cnt⟩
apply xD.2
exact mem_biUnion this xU
by_contra! h
exact absurd (Countable.mono h (Set.countable_singleton _)) this
· rw [inter_comm, inter_union_diff]
