mem_closure_iff_nhds_ne_bot — Mathlib

English

x ∈ closure s iff nhds x intersects s nontrivially in every neighborhood.

Русский

x принадлежит замыканию s тогда и только тогда, когда во всех окрестностях x пересечение nhds x с s не пусто.

LaTeX

$$$x \in \overline{s} \iff \forall t \in \mathcal{N}(x),\ (t \cap s) \neq \emptyset$$$

Lean4

theorem mem_closure_iff_nhds_ne_bot : x ∈ closure s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥ :=
  mem_closure_iff_clusterPt.trans neBot_iff

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