t5Space — Mathlib

English

Let X be a linearly ordered set endowed with the order topology. Then X is a T5 space (completely normal).

Русский

Пусть X — линейно упорядоченное множество, оснащённое порядковой топологией. Тогда X является T5-пространством (полностью нормальным).

LaTeX

$$$\forall X\left(\mathrm{LinearOrder}(X) \land \mathrm{TopologicalSpace}(X) \land \mathrm{OrderTopology}(X)\right) \Rightarrow \mathrm{T5Space}(X)$$$

Lean4

instance (priority := 100) t5Space : T5Space X :=
  T5Space.mk

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