r1Space — Mathlib

English

Hausdorff property is equivalent to a criterion using ultrafilters: if two ultrafilters map below nhds x and nhds y respectively, then x = y.

Русский

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

LaTeX

$$$ [T2Space X] \iff \forall x,y\ (f : Ultrafilter X), f \lenhds x \to f \le nhds y \to x=y $$$

Lean4

instance (priority := 100) r1Space [T2Space X] : R1Space X :=
  ⟨fun x y ↦ (eq_or_ne x y).imp specializes_of_eq disjoint_nhds_nhds.2⟩

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