cocompact_eq_atBot_atTop — Mathlib

English

In a NoMaxOrder NoMinOrder OrderClosedTopology CompactIccSpace, cocompact α equals the join of atBot and atTop: cocompact α = atBot ⊔ atTop.

Русский

В пространстве без максимума и без минимума с OrderClosedTopology и CompactIccSpace коккомпактность равна объединению нижнего и верхнего концов: cocompact α = atBot ⊔ atTop.

LaTeX

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

Lean4

@[simp 900]
theorem cocompact_eq_atBot_atTop [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] :
    cocompact α = atBot ⊔ atTop :=
  cocompact_le_atBot_atTop.antisymm atBot_atTop_le_cocompact

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