linearGrowthSup_comp_nonneg — Mathlib

English

If u is monotone and not bottom, then linearGrowthSup(u ∘ v) ≥ 0, whenever v grows appropriately and hv-spaces hold; in particular 0 ≤ linearGrowthSup(u ∘ v).

Русский

Если u монотонна и не нижняя, то линейный верхний рост композиции неотрицателен: 0 ≤ linearGrowthSup(u ∘ v).

LaTeX

$$$0 \le \operatorname{linearGrowthSup}(u \circ v)$$$

Lean4

theorem linearGrowthSup_comp_nonneg (h : Monotone u) (h' : u ≠ ⊥) (hv : Tendsto v atTop atTop) :
    0 ≤ linearGrowthSup (u ∘ v) :=
  (linearGrowthInf_comp_nonneg h h' hv).trans linearGrowthInf_le_linearGrowthSup

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