le_linearGrowthSup — Mathlib

English

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

Русский

Если существует бесконечное множество n таких, что a n ≤ u(n), то a ≤ linearGrowthSup(u).

LaTeX

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

Lean4

theorem _root_.Frequently.le_linearGrowthSup (h : ∃ᶠ n : ℕ in atTop, a * n ≤ u n) : a ≤ linearGrowthSup u :=
  le_linearGrowthSup_iff.2 fun c c_u ↦ h.mono fun n hn ↦ hn.trans' <| by gcongr

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