expGrowthSup_nonneg — Mathlib

English

If a monotone ENNReal sequence u is nonzero, then 0 ≤ expGrowthSup u.

Русский

Если монотонная последовательность u в ENNReal не равна нулю, то 0 ≤ expGrowthSup u.

LaTeX

$$$0 \le \expGrowthSup(u) \quad\text{when } \text{Monotone}(u) \text{ and } u \neq 0$$$

Lean4

theorem _root_.Monotone.expGrowthSup_nonneg (h : Monotone u) (h' : u ≠ 0) : 0 ≤ expGrowthSup u :=
  (h.expGrowthInf_nonneg h').trans expGrowthInf_le_expGrowthSup

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