of_frequently_ge — Mathlib

English

In linear orders, frequent lower-bounding implies coboundedness for ≤.

Русский

В линейном порядке частотное ограничение снизу влечёт coboundedness относительно ≤.

LaTeX

$$$\text{If } freq\_ge \text{ holds for } f, \text{ then } IsCobounded(≤) f.$$$

Lean4

/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`. -/
theorem of_frequently_ge [LinearOrder α] {l : α} (freq_ge : ∃ᶠ x in f, l ≤ x) : IsCobounded (· ≤ ·) f :=
  by
  rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
  · exact ⟨l, fun x _ ↦ lbot x⟩
  refine ⟨l', fun u hu ↦ ?_⟩
  obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists
  exact hl'.le.trans (l_le_w.trans w_le_u)

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