linearGrowthSup_monotone — Mathlib

English

If u ≤ v holds for all n, then linearGrowthSup(u) ≤ linearGrowthSup(v).

Русский

Если для всех n выполняется u(n) ≤ v(n), то linearGrowthSup(u) ≤ linearGrowthSup(v).

LaTeX

$$$\bigl( \forall n \in \mathbb{N},\; u(n) \le v(n) \bigr) \implies \operatorname{linearGrowthSup}(u) \le \operatorname{linearGrowthSup}(v).$$$

Lean4

theorem linearGrowthSup_monotone (h : u ≤ v) : linearGrowthSup u ≤ linearGrowthSup v :=
  linearGrowthSup_eventually_monotone (Eventually.of_forall h)

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