t2_iff_isClosed_diagonal — Mathlib

English

A space is Hausdorff iff the diagonal in X × X is closed.

Русский

Пространство является хаусдорфовым тогда и только тогда, когда диагональ в X × X замкнута.

LaTeX

$$$ \operatorname{T2Space}(X) \iff \operatorname{IsClosed}(\Delta_X) $$$

Lean4

theorem t2_iff_isClosed_diagonal : T2Space X ↔ IsClosed (diagonal X) := by
  simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall, nhds_prod_eq,
    compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff, Pairwise]

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