English
Let s be a subset of X. Then x is a cluster point of the principal filter generated by s if and only if every neighborhood U of x meets s nontrivially (i.e., U ∩ s ≠ ∅).
Русский
Пусть s ⊆ X. Тогда x является кластерной точкой Principal(s) тогда и только тогда, когда любая окрестность U(x) пересекает s не пусто.
LaTeX
$$$\\mathrm{ClusterPt}(x, \\mathcal{P}(s)) \\iff \\forall U \\in \\mathcal{N}(x),\n\\ (U \\cap s) \\neq \\emptyset$$$
Lean4
/-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty
set. See also `mem_closure_iff_clusterPt`. -/
theorem clusterPt_principal_iff : ClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty :=
inf_principal_neBot_iff
