English
Let x be a point in a topological space and C a subset. Then x is an accumulation point of C if and only if every neighborhood of x contains a point of C different from x.
Русский
Пусть x — точка в топологическом пространстве и C — подмножество. Тогда x является накопленной точкой множества C тогда и только тогда, когда каждая окрестность x содержит точку из C, отличную от x.
LaTeX
$$$x \in \overline{C \setminus \{x\}} \iff \forall U \in \mathcal{N}(x),\ (U \setminus \{x\}) \cap C \neq \emptyset$$$
Lean4
/-- `x` is an accumulation point of a set `C` iff every neighborhood
of `x` contains a point of `C` other than `x`. -/
theorem accPt_iff_nhds {x : X} {C : Set X} : AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x := by
simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff, Set.Nonempty, and_assoc]
