eventually_exp_le — Mathlib

English

If a < expGrowthInf u, then exp(a n) ≤ u(n) holds for all sufficiently large n.

Русский

Если a < expGrowthInf(u), то существует N, что для всех n ≥ N выполняется exp(a n) ≤ u(n).

LaTeX

$$$a < \expGrowthInf(u) \Rightarrow \exists N \forall n \ge N,\ \exp(a n) \le u(n)$$$

Lean4

theorem eventually_exp_le (h : a < expGrowthInf u) : ∀ᶠ n : ℕ in atTop, exp (a * n) ≤ u n :=
  le_expGrowthInf_iff.1 (le_refl (expGrowthInf u)) a h

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