to_t2Space — Mathlib

English

A linearly ordered set endowed with an OrderClosedTopology is a Hausdorff (T2) space.

Русский

Линейно упорядоченное множество с топологией OrderClosedTopology является эрзац-хаусдорфовым пространством (T2).

LaTeX

$$$ \\text{If } \\alpha \\text{ is a linear order with OrderClosedTopology, then } \\alpha \\text{ is a } T_2\\text{ space.}$$$

Lean4

instance (priority := 90) to_t2Space : T2Space α :=
  t2_iff_isClosed_diagonal.2 <| by
    simpa only [diagonal, le_antisymm_iff] using t.isClosed_le'.inter (isClosed_le continuous_snd continuous_fst)

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