le_linearGrowthInf — Mathlib

English

If u(n) ≥ a n eventually, then a ≤ linearGrowthInf(u).

Русский

Если для больших n выполнено u(n) ≥ a n, то a ≤ linearGrowthInf(u).

LaTeX

$$$\bigl( \forall^{\infty} n,\; a \cdot n \le u(n) \bigr) \implies a \le \operatorname{linearGrowthInf}(u).$$$

Lean4

theorem _root_.Eventually.le_linearGrowthInf (h : ∀ᶠ n : ℕ in atTop, a * n ≤ u n) : a ≤ linearGrowthInf u :=
  le_linearGrowthInf_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr

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