English
Let x be a point and C a subset. Then x is an accumulation point of C iff there are points y ≠ x with y ∈ C that occur frequently in neighborhoods of x.
Русский
Пусть x — точка и C — подмножество. Тогда x является накопленной точкой C тогда и только тогда, когда существуют точки y ≠ x с y ∈ C, которые часто встречаются в окрестностях x.
LaTeX
$$$x \in \overline{C \setminus \{x\}} \iff \exists^{\mathrm{f}} y \in \mathcal{N}(x),\ y \neq x \land y \in C$$$
Lean4
/-- `x` is an accumulation point of a set `C` iff
there are points near `x` in `C` and different from `x`. -/
theorem accPt_iff_frequently {x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C := by
simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff_frequently, and_comm]
