expGrowthSup_sup — Mathlib

English

For sequences u, v, expGrowthSup(u ⊔ v) = expGrowthSup(u) ⊔ expGrowthSup(v).

Русский

Для последовательностей u, v: expGrowthSup(u ⊔ v) = expGrowthSup(u) ⊔ expGrowthSup(v).

LaTeX

$$$\expGrowthSup(u \lor v) = \expGrowthSup(u) \lor \expGrowthSup(v)$$$

Lean4

theorem expGrowthSup_sup : expGrowthSup (u ⊔ v) = expGrowthSup u ⊔ expGrowthSup v :=
  by
  rw [expGrowthSup, expGrowthSup, expGrowthSup, ← limsup_max]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.sup_apply, log_monotone.map_max]
  exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

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