English
Let f : β → γ → α and suppose that uncurry f is Multipliable, and for every b ∈ β the sequence c ↦ f(b, c) is Multipliable. Then the double product over β × γ equals the iterated product: ∏' p, uncurry f p = ∏' b ∈ β ∏' c ∈ γ, f(b, c).
Русский
Пусть f : β → γ → α и uncurry f умножаемо; пусть для каждого b ∈ β функция c ↦ f(b, c) множима; тогда бесконечное произведение по всем парам равно итеративному произведению: ∏' p, uncurry f p = ∏' b ∈ β ∏' c ∈ γ, f(b, c).
LaTeX
$$$$ \prod' p : β \times γ, \mathrm{uncurry}\, f(p) = \prod' b \; \prod' c, f(b, c). $$$$
Lean4
@[to_additive Summable.tsum_prod_uncurry]
protected theorem tprod_prod_uncurry {f : β → γ → α} (h : Multipliable (Function.uncurry f))
(h₁ : ∀ b, Multipliable fun c ↦ f b c) : ∏' p : β × γ, uncurry f p = ∏' (b) (c), f b c :=
(h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm
