disjoint_nhdsSet_nhds — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem disjoint_nhdsSet_nhds : Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s :=
  by
  have h := (regularSpace_TFAE X).out 0 2
  exact h.mp ‹_› _ _

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