English
For nontrivial linear orders, coboundedness for ≤ implies frequent lower-bounding from below.
Русский
Для ненулевого линейного порядка, кобундированность по ≤ влечёт частотное ограничение снизу.
LaTeX
$$$\text{If } f \text{ is cobounded under } (\le) \text{ on a linear order, then } \exists l, \exists^\! x \in f, l \le x.$$$
Lean4
/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
from below. -/
theorem frequently_ge [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≤ ·) f) : ∃ l, ∃ᶠ x in f, l ≤ x :=
by
obtain ⟨t, ht⟩ := cobdd
rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
· exact ⟨t, .of_forall fun r ↦ tbot r⟩
refine ⟨t', fun ev ↦ ?_⟩
specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
exact not_lt_of_ge ht ht'
