sum_sum_index' — Mathlib

English

Sum-sum interchange: for h0 and h1 as in the theorem, (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t.

Русский

Замена порядков сумм: сумма над s затем сумма по t эквивалентны сумме по x над s от суммы f x по t.

LaTeX

$$$\big(\sum_{x \in s} f_x\big).sum t = \sum_{x \in s} (f_x).sum t.$$$

Lean4

theorem sum_sum_index' (h0 : ∀ i, t i 0 = 0) (h1 : ∀ i x y, t i (x + y) = t i x + t i y) :
    (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t := by
  classical
    exact
    Finset.induction_on s rfl fun a s has ih => by simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]

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