expGrowthInf_iInf — Mathlib

English

Same pattern as above for a finite family: expGrowthInf(iInf i => u_i) = iInf i => expGrowthInf(u_i).

Русский

Та же конструкция для конечной семейства: expGrowthInf(iInf i => u_i) = iInf i => expGrowthInf(u_i).

LaTeX

$$$\expGrowthInf\left(\iInf i, u_i\right) = \iInf i, \expGrowthInf(u_i)$$$

Lean4

theorem expGrowthInf_iInf {ι : Type*} [Finite ι] (u : ι → ℕ → ℝ≥0∞) :
    expGrowthInf (⨅ i, u i) = ⨅ i, expGrowthInf (u i) := by
  rw [← iInf_univ, expGrowthInf_biInf u Set.finite_univ, iInf_univ]

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