isBoundedUnder_of_eventually_ge — Mathlib

English

If ∀ᶠ x in f, a ≤ u x, then f is bounded under ≥ by u with bound a.

Русский

Если существует a такое, что почти все x удовлетворяют a ≤ u x, тогда f ограничен по ≥ через u сверху границей a.

LaTeX

$$$ (h : ∀^\infty x \text{ in } f, a ≤ u x) \Rightarrow IsBoundedUnder (\ge) f u $$$

Lean4

theorem isBoundedUnder_of_eventually_ge {a : α} (h : ∀ᶠ x in f, a ≤ u x) : IsBoundedUnder (· ≥ ·) f u :=
  ⟨a, h⟩

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