English
Let α be a linear order with OrderTop and CompactIccSpace. Then the cocompact filter is bounded above by the bottom-top join; concretely, cocompact α ≤ atBot ⊔ atTop.
Русский
Пусть α — линейный порядок с OrderTop и CompactIccSpace. Тогда коккомпактный фильтр ограничен снизу объединением точек: cocompact α ≤ atBot ⊔ atTop.
LaTeX
$$$\text{cocompact}(\alpha) \le atBot \sqcup atTop$$$
Lean4
theorem cocompact_le_atBot [OrderTop α] [CompactIccSpace α] : cocompact α ≤ atBot :=
by
refine fun _ hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
· exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
· obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs
refine ⟨Icc t ⊤, isCompact_Icc, fun _ hx ↦ ?_⟩
exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)
