linearGrowthSup_le — Mathlib

English

If u(n) ≤ a n for all large n, then linearGrowthSup(u) ≤ a.

Русский

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

LaTeX

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

Lean4

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

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