disjoint_nhds_pure — Mathlib

English

In a T1 space, for any distinct x,y, the neighborhoods nhds x and the pure filter at y are disjoint.

Русский

В T1-пространстве для любых x ≠ y окрестности nhds x и чистый фильтр в y единообразно не пересекаются.

LaTeX

$$$\\forall X [\\mathcal{T}_1(X)], \\forall x,y\\ (x\\neq y) \\Rightarrow Disjoint(nhds(x), pure(y)).$$$

Lean4

theorem disjoint_nhds_pure [T1Space X] {x y : X} (h : x ≠ y) : Disjoint (𝓝 x) (pure y) :=
  t1Space_iff_disjoint_nhds_pure.mp ‹_› h

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