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]