linearGrowthInf_eventually_monotone

English

If u ≤ᶠ[atTop] v (u eventually bounded above by v), then linearGrowthInf(u) ≤ linearGrowthInf(v).

Русский

Если u ≤ᶠ[atTop] v, то нижний линейный темп роста u не превосходит темп роста v.

LaTeX

$$$ \\text{linearGrowthInf} (u) \\le \\text{linearGrowthInf} (v) $$$

Lean4

theorem linearGrowthInf_eventually_monotone (h : u ≤ᶠ[atTop] v) : linearGrowthInf u ≤ linearGrowthInf v :=
  liminf_le_liminf (h.mono fun n u_v ↦ EReal.monotone_div_right_of_nonneg n.cast_nonneg' u_v)

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