eventually_ge — Mathlib

English

Similarly, if f is bounded under ≥ by u, there exists a bound a with a ≤ u x eventually.

Русский

Аналогично, если f ограничен снизу по ≥ через u, существует граница a такая, что a ≤ u x выполняется почти наверняка.

LaTeX

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

Lean4

theorem eventually_ge (h : IsBoundedUnder (· ≥ ·) f u) : ∃ a, ∀ᶠ x in f, a ≤ u x :=
  IsBoundedUnder.eventually_le (α := αᵒᵈ) h

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