eventually_mul_le — Mathlib

English

If there are infinitely many n with u(n) ≤ a n, then linearGrowthInf(u) ≤ a.

Русский

Если существует бесконечное число n такое, что u(n) ≤ a n, то линейный инфим линейного роста не превышает a.

LaTeX

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

Lean4

theorem eventually_mul_le (h : a < linearGrowthInf u) : ∀ᶠ n : ℕ in atTop, a * n ≤ u n :=
  le_linearGrowthInf_iff.1 (le_refl (linearGrowthInf u)) a h

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