mem_closure_ne_iff_frequently_within

English

Characterization of z in closure of s \ {z} via frequently within nhds within sn.

Русский

Характеризация того, что z лежит в замыкании множества s без z через часто посещения внутри nhdsWithin.

LaTeX

$$$z ∈ \overline{(s \ {z})} ⇔ ∃ᶠ x in 𝓝[\neq] z, x ∈ s$$$

Lean4

theorem mem_closure_ne_iff_frequently_within {z : α} {s : Set α} : z ∈ closure (s \ { z }) ↔ ∃ᶠ x in 𝓝[≠] z, x ∈ s := by
  simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

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