map_update_sum — Mathlib

English

Let f be multilinear; then summing over all indices i of a family of inputs equals the sum over all index functions r of f evaluated at the corresponding coordinates.

Русский

Пусть f мультиленейная; тогда сумма по всем координатам индексов эквивалентна сумме по всем функциям индексов r.

LaTeX

$$$ f ( (\\text{univ}) ) = \\sum_{r} f( ... ) $$$

Lean4

theorem map_update_sum {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M₁ i) (m : ∀ i, M₁ i) :
    f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a)) := by
  classical
    induction t using Finset.induction with
  | empty => simp
  | insert _ _ has ih => simp [Finset.sum_insert has, ih]

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