finprod_curry₃ — Mathlib

English

If f: α × β × γ → M has finite mulSupport, then the triple finsum equals the triple nested finsum: ∏ᶠ abc, f abc = ∏ᶠ a, b, c, f(a,b,c).

Русский

Если f: α × β × γ → M имеет конечную мультиподдержку, то тройное finsum равно тройному вложенному finsum.

LaTeX

$$$ (\\\\prod^\\\\mathrm{f} abc, f(abc)) = \\\\prod^\\\\mathrm{f} a (b) (c), f(a,b,c) $$$

Lean4

@[to_additive]
theorem finprod_curry₃ {γ : Type*} (f : α × β × γ → M) (h : (mulSupport f).Finite) :
    ∏ᶠ abc, f abc = ∏ᶠ (a) (b) (c), f (a, b, c) :=
  by
  rw [finprod_curry f h]
  congr
  ext a
  rw [finprod_curry]
  simp [h]

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