English
If α has no minimum and is closed under downward limits, then every downward ray is cocompact: atBot ≤ cocompact α.
Русский
Если у α нет минимума и она замкнута по нисходящей, то каждая нисходящая лучевая область коккомпактна: atBot ≤ cocompact α.
LaTeX
$$$\\text{atBot} \\le \\text{cocompact}(\\alpha)$$$
Lean4
theorem atBot_le_cocompact [NoMinOrder α] [ClosedIicTopology α] : atBot ≤ cocompact α :=
by
refine fun s hs ↦ ?_
obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
refine (Set.eq_empty_or_nonempty t).casesOn (fun h_empty ↦ ?_) (fun h_nonempty ↦ ?_)
· rewrite [compl_univ_iff.mpr h_empty, univ_subset_iff] at hts
convert univ_mem
· haveI := h_nonempty.nonempty
obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
obtain ⟨b, hb⟩ := exists_lt a
exact
Filter.mem_atBot_sets.mpr
⟨b, fun b' hb' ↦
hts <|
Classical.byContradiction fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩
