English
A point x is an accumulation point of C iff there are frequently points y ∈ C with y ≠ x in the punctured neighborhoods of x.
Русский
Точка x является накопленной точкой C тогда и только тогда, когда в проколотых окрестностях x встречаются часто точки y ∈ C с y ≠ x.
LaTeX
$$$x \in \overline{C \setminus \{x\}} \iff \exists^{\mathrm{f}} y \in \mathcal{N}_{\neq x}(x),\ y \in C$$
Lean4
/-- Variant of `accPt_iff_frequently`: A point `x` is an accumulation point of a set `C` iff points in
punctured neighborhoods are frequently contained in `C`.
-/
theorem accPt_iff_frequently_nhdsNE {X : Type*} [TopologicalSpace X] {x : X} {C : Set X} :
AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C :=
by
have : (∃ᶠ z in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ z in 𝓝 x, z ∈ C ∧ z ∈ ({ x } : Set X)ᶜ :=
frequently_inf_principal.trans <| by simp only [and_comm]
rw [accPt_iff_frequently, this]
congr! 2
tauto
