cocompact_le_atTop — Mathlib

English

In a linearly ordered α with NoMaxOrder and CompactIccSpace, the cocompact filter is bounded above by atTop; equivalently, every cocompact set contains a tail to the top.

Русский

В линейном порядке α с NoMaxOrder и CompactIccSpace коккомпактный фильтр ограничен сверху atTop; то есть каждая кокомпактная подмножество содержит хвост к верхнему концу.

LaTeX

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

Lean4

theorem cocompact_le_atTop [OrderBot α] [CompactIccSpace α] : cocompact α ≤ atTop :=
  cocompact_le_atBot (α := αᵒᵈ)

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