cocompact_eq_atTop — Mathlib

English

In a NoMinOrder α with CompactIccSpace and OrderTop, cocompact α equals atBot ⊔ atTop.

Русский

В NoMinOrder α с CompactIccSpace и OrderTop коккомпактность равна объединению нижнего и верхнего концов.

LaTeX

$$$\\text{cocompact}(\\alpha) = \\text{atBot} \\sqcup \\text{atTop}$$$

Lean4

@[simp]
theorem cocompact_eq_atTop [NoMaxOrder α] [OrderBot α] [ClosedIciTopology α] [CompactIccSpace α] :
    cocompact α = atTop :=
  cocompact_le_atTop.antisymm atTop_le_cocompact

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