expGrowthSup_iSup — Mathlib

English

For finite ι and u: ι → ℕ → ℝ≥0∞, expGrowthSup (iSup i, u i) = iSup i, expGrowthSup(u i).

Русский

Для конечного индекса i и семейства u_i: expGrowthSup(iSup_i u_i) = iSup_i expGrowthSup(u_i).

LaTeX

$$$\expGrowthSup\left(\iSup i, u_i\right) = \iSup i, \expGrowthSup(u_i)$$$

Lean4

theorem expGrowthSup_iSup {ι : Type*} [Finite ι] (u : ι → ℕ → ℝ≥0∞) :
    expGrowthSup (⨆ i, u i) = ⨆ i, expGrowthSup (u i) := by
  rw [← iSup_univ, expGrowthSup_biSup u Set.finite_univ, iSup_univ]

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