English
Let x ∈ X and s ⊆ X. Then x ∈ closure(s) iff x ∈ s frequently with respect to 𝓝(x).
Русский
Пусть x ∈ X и s ⊆ X. Тогда x ∈ closure(s) тогда и только тогда, когда x встречается в s часто относительно 𝓝(x).
LaTeX
$$$x \\in \\overline{s} \\iff \\exists^\\mathrm{f} y \\in \\mathcal{N}(x), y \\in s$$$
Lean4
theorem mem_closure_iff_frequently : x ∈ closure s ↔ ∃ᶠ x in 𝓝 x, x ∈ s := by
rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds, closure_eq_compl_interior_compl, mem_compl_iff,
compl_def]