t2_iff_ultrafilter — Mathlib

English

Hausdorff property is equivalent to a criterion using ultrafilters: for every ultrafilter f, if f ≤ nhds x and f ≤ nhds y, then x = y.

Русский

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

LaTeX

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

Lean4

theorem t2_iff_ultrafilter : T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y :=
  t2_iff_nhds.trans <| by simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

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