sum_uncurry_index' — Mathlib

English

For f: α × β →₀ M and g: α → β → M → N, the twofold currying-summing equality holds: f.curry.sum (λ a f, f.sum (λ b, g a b)) = f.sum (λ p c, g p.1 p.2 c).

Русский

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

LaTeX

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

Lean4

theorem sum_uncurry_index' [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α → β → M → N) :
    f.uncurry.sum (fun p c => g p.1 p.2 c) = f.sum fun a f => f.sum (g a) :=
  sum_uncurry_index ..

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