English
In a T1 space, a preperfect set C has a closure that is perfect; equivalently, Preperfect C implies Perfect (closure C).
Русский
В T1-пространстве замыкание предперфектного множества является совершенным; то есть Preperfect C влечёт Perfect (closure C).
LaTeX
$$$\text{Preperfect}(C) \implies \text{Perfect}(\overline{C}).$$$
Lean4
/-- A set `C` is preperfect if all of its points are accumulation points of itself.
If `α` is a T1 space, this is equivalent to the closure of `C` being perfect,
see `preperfect_iff_perfect_closure`. This property is also called dense-in-itself. -/
def Preperfect (C : Set α) : Prop :=
∀ x ∈ C, AccPt x (𝓟 C)
