t2_iff_nhds — Mathlib

English

Hausdorff property is equivalent to a neighborhood intersection criterion: if nhds x and nhds y intersect nontrivially, then x=y.

Русский

Свойство Хаусдорфа эквивалентно условию через пересечение окрестностей: если nhds x и nhds y пересекаются не тривиально, то x=y.

LaTeX

$$$ [T2Space X] \iff \forall x,y\, \operatorname{NeBot}(\mathcal{N}(x) \cap \mathcal{N}(y)) \Rightarrow x=y $$$

Lean4

/-- A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter. -/
theorem t2_iff_nhds : T2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y := by
  simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne, not_imp_comm, Pairwise]

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