t2Space — Mathlib

English

For every α, the space Ultrafilter α is a Hausdorff space.

Русский

Для любого пространства α пространство Ultrafilter α является гaусдорфовым.

LaTeX

$$$T2Space\left(Ultrafilter\ α\right)$$$

Lean4

instance t2Space : T2Space (Ultrafilter α) :=
  t2_iff_ultrafilter.mpr fun {x y} f fx fy ↦
    have hx : x = joinM f := ultrafilter_converges_iff.mp fx
    have hy : y = joinM f := ultrafilter_converges_iff.mp fy
    hx.trans hy.symm

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