English
In a sufficiently nice space, a perfect nonempty set can be split into two disjoint nonempty perfect subsets, each contained in the original set.
Русский
В достаточно хорошем пространстве совершенное ненулевое множество можно разложить на две непустые взаимно непересекающиеся совершенные подмножества, вложенные в исходное множество.
LaTeX
$$$\exists C_0, C_1 \subseteq C,\; \text{Perfect}(C_0) \land C_0\neq \emptyset \land C_0\subseteq C \land \text{Perfect}(C_1) \land C_1\neq \emptyset \land C_1\subseteq C \land \text{Disjoint}(C_0,C_1).$$$
Lean4
/-- In a T1 space, being preperfect is equivalent to having perfect closure. -/
theorem preperfect_iff_perfect_closure [T1Space α] : Preperfect C ↔ Perfect (closure C) :=
by
constructor <;> intro h
· exact h.perfect_closure
intro x xC
have H : AccPt x (𝓟 (closure C)) := h.acc _ (subset_closure xC)
rw [accPt_iff_frequently] at *
have : ∀ y, y ≠ x ∧ y ∈ closure C → ∃ᶠ z in 𝓝 y, z ≠ x ∧ z ∈ C :=
by
rintro y ⟨hyx, yC⟩
simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff, hyx.nhdsWithin_compl_singleton,
← mem_closure_iff_frequently]
exact yC
rw [← frequently_frequently_nhds]
exact H.mono this
