expGrowthSup_biSup — Mathlib

English

For a finite set s and u : α → ℕ → ℝ≥0∞, expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x).

Русский

Для конечного множества s верно: expGrowthSup(⨆ x∈s, u x) = ⨆ x∈s, expGrowthSup(u x).

LaTeX

$$$\expGrowthSup\left(\bigvee_{x\in s} u_x\right) =\bigvee_{x\in s} \expGrowthSup(u_x)$$$

Lean4

theorem expGrowthSup_biSup {α : Type*} (u : α → ℕ → ℝ≥0∞) {s : Set α} (hs : s.Finite) :
    expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x) :=
  by
  have := map_finset_sup expGrowthSupBotHom hs.toFinset u
  simpa only [expGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup, hs.mem_toFinset, comp_apply]

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