cocompact_eq_atBot — Mathlib

English

Under NoMaxOrder NoMinOrder OrderClosedTopology CompactIccSpace, cocompact α equals atTop.

Русский

При NoMaxOrder NoMinOrder OrderClosedTopology CompactIccSpace коккомпактность совпадает с atTop.

LaTeX

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

Lean4

@[simp]
theorem cocompact_eq_atBot [NoMinOrder α] [OrderTop α] [ClosedIicTopology α] [CompactIccSpace α] :
    cocompact α = atBot :=
  cocompact_le_atBot.antisymm atBot_le_cocompact

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