mem_closure_iff_frequently — Mathlib

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]

Похожие утверждения