of_compactSpace_r1Space — Mathlib

English

If X is compact and T1, then X is a normal space.

Русский

Пусть X — компактное пространство и T1; тогда X нормальное пространство.

LaTeX

$$$ \\text{CompactSpace}(X) \\land \\text{R1Space}(X) \\Rightarrow \\text{NormalSpace}(X). $$$

Lean4

instance (priority := 100) of_compactSpace_r1Space [CompactSpace X] [R1Space X] : NormalSpace X where
  normal _s _t hs ht := .of_isCompact_isCompact_isClosed hs.isCompact ht.isCompact ht

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