English
In a linear order α with CompactIccSpace, every cocompact set s contains a nonempty compact interval Icc(t,u); equivalently, cocompact α ≤ atBot ⊔ atTop.
Русский
В линейном порядке α с свойством CompactIccSpace любая кокомпактная подмножество содержит не пустой компактный интервал Icc(t,u); эквивалентно cocompact α ≤ atBot ⊔ atTop.
LaTeX
$$$\text{cocompact}(\alpha) \le atBot \sqcup atTop$$$
Lean4
theorem cocompact_le_atBot_atTop [CompactIccSpace α] : cocompact α ≤ atBot ⊔ atTop :=
by
refine fun s 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.1
obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)
