English
In a topological space, a set C is preperfect if and only if every point x in C has every neighborhood U of x containing some y ≠ x with y ∈ C.
Русский
Во множестве C предперфектно тогда и только тогда, когда для каждого x ∈ C и любого окружения U x найдется y ≠ x с y ∈ C и y ∈ U.
LaTeX
$$$\text{Preperfect}(C) \iff \forall x\in C, \forall U\in \mathcal{N}(x), \exists y \in U \cap C, y \neq x.$$$
Lean4
theorem preperfect_iff_nhds : Preperfect C ↔ ∀ x ∈ C, ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
simp only [Preperfect, accPt_iff_nhds]