disjoint_nhds_nhdsSet — Mathlib

English

In a regular space, the neighborhoods of a point x and the nhdsSet of s are disjoint if and only if x is not in the closure of s.

Русский

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

LaTeX

$$$Disjoint \, (\mathcal N(x)) \, (\mathcal{N}\!\!\mathrm{ˢ}(s)) \iff x \notin \overline{s}$$$

Lean4

theorem disjoint_nhds_nhdsSet : Disjoint (𝓝 x) (𝓝ˢ s) ↔ x ∉ closure s :=
  disjoint_comm.trans disjoint_nhdsSet_nhds

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