expGrowthInf_biInf — Mathlib

English

For a finite index set ι, expGrowthInf(iInf i => u_i) = iInf i => expGrowthInf(u_i).

Русский

Для конечного индексного множества i: expGrowthInf( iInf i, u(i) ) = iInf i, expGrowthInf(u(i)).

LaTeX

$$$\expGrowthInf\left(\inf_{i} u_i\right) = \inf_{i} \expGrowthInf(u_i)$$$

Lean4

theorem expGrowthInf_biInf {α : Type*} (u : α → ℕ → ℝ≥0∞) {s : Set α} (hs : s.Finite) :
    expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x) :=
  by
  have := map_finset_inf expGrowthInfTopHom hs.toFinset u
  simpa only [expGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf, hs.mem_toFinset, comp_apply]

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