linearGrowthInf_le — Mathlib

English

If u(n) ≤ a n holds for infinitely many n, then linearGrowthInf(u) ≤ 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 _root_.Frequently.linearGrowthInf_le (h : ∃ᶠ n : ℕ in atTop, u n ≤ a * n) : linearGrowthInf u ≤ a :=
  linearGrowthInf_le_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans <| by gcongr

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