sum_uncurry_index — Mathlib

English

For f: α →₀ β →₀ M and g: α × β → M → N, the identity f.uncurry.sum (λ p c, g p c) equals f.sum (λ a f, f.sum (λ b, g (a,b))).

Русский

Для f: α →₀ β →₀ M и g: α×β → M→N выполняется равенство: f.uncurry.sum (λ p c, g p c) = f.sum (λ a f, f.sum (λ b, g (a,b))).

LaTeX

$$$f.uncurry.sum(\lambda p\, c.\, g\,p\,c) = f.sum(\lambda a\, f.\, f.sum(\lambda b.\, g (a,b)))$$$

Lean4

theorem sum_uncurry_index [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α × β → M → N) :
    f.uncurry.sum (fun p c => g p c) = f.sum fun a f => f.sum fun b ↦ g (a, b) := by
  simp [Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion]

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