sum_curry_index — Mathlib

English

The double-sum identity holds: (f: α×β →₀ M).curry.sum (λ a f, f.sum (λ b, g a b)) equals f.sum (λ p c, g p.1 p.2 c).

Русский

Двойная сумма удовлетворяет тождеству: (f: α×β →₀ M).curry.sum (λ a f, f.sum (λ b, g a b)) = f.sum (λ p c, g p.1 p.2 c).

LaTeX

$$$\bigl(f.\text{curry}.\sum (\lambda a\ f.\, f.\sum (\lambda b.\, g\,a\,b))\bigr) = f.\sum (\lambda p\ c.\, g\,p.1\,p.2\,c)$$$

Lean4

theorem sum_curry_index [AddCommMonoid N] (f : α × β →₀ M) (g : α → β → M → N) :
    (f.curry.sum fun a f => f.sum (g a)) = f.sum fun p c => g p.1 p.2 c := by rw [← sum_uncurry_index', uncurry_curry]

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