expGrowthSup_eventually_monotone — Mathlib

English

expGrowthSup_eventually_monotone: if u ≤ᶠ v, then expGrowthSup u ≤ expGrowthSup v.

Русский

expGrowthSup_eventually_monotone: если u ≤ᶠ v, то expGrowthSup u ≤ expGrowthSup v.

LaTeX

$$$u \\leq^{{atTop}} v \\Rightarrow \\expGrowthSup(u) \\leq \\expGrowthSup(v).$$$

Lean4

theorem expGrowthSup_eventually_monotone (h : u ≤ᶠ[atTop] v) : expGrowthSup u ≤ expGrowthSup v :=
  limsup_le_limsup (h.mono fun n uv ↦ monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone uv))

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