English
For a finite set s and u: α → ℕ → ℝ≥0∞, expGrowthSup (∑ x∈s, u x) = ⨆ x∈s, expGrowthSup(u x).
Русский
Для конечного множества s и семейства u: expGrowthSup (∑ x∈s, u x) = ⨆ x∈s, expGrowthSup(u x).
LaTeX
$$$\expGrowthSup\left(\sum_{x\in s} u_x\right) = \bigvee_{x\in s} \expGrowthSup(u_x)$$$
Lean4
theorem expGrowthSup_sum {α : Type*} (u : α → ℕ → ℝ≥0∞) (s : Finset α) :
expGrowthSup (∑ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x) := by
classical
induction s using Finset.induction_on with
| empty => rw [Finset.sum_empty, ← Finset.iSup_coe, Finset.coe_empty, iSup_emptyset, expGrowthSup_zero]
| insert a t a_t ha =>
rw [Finset.sum_insert a_t, expGrowthSup_add, ← Finset.iSup_coe, Finset.coe_insert a t, iSup_insert, Finset.iSup_coe,
ha]
