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]