expGrowthInf_nonneg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.Monotone.expGrowthInf_nonneg (h : Monotone u) (h' : u ≠ 0) : 0 ≤ expGrowthInf u :=
  by
  apply (log_monotone.comp h).linearGrowthInf_nonneg
  simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢
  exact h'

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