English
If uncurry f is Multipliable, and for all b the fiber f(b) is Multipliable as a function of c, and for all c the function b ↦ f(b, c) is Multipliable, then the double fiberwise product is symmetric: ∏' (c) (b), f(b, c) = ∏' (b) (c), f(b, c).
Русский
Если uncurry f множимо, и для каждого b функция c ↦ f(b, c) множима, и для каждого c функция b ↦ f(b, c) множима, то двоичное произведение по отношению к порядку сомножителей не зависит от порядка: ∏' (c) (b) f(b, c) = ∏' (b) (c) f(b, c).
LaTeX
$$$$ \prod' c \; \prod' b, f(b,c) = \prod' b \; \prod' c, f(b,c). $$$$
Lean4
@[to_additive]
protected theorem tprod_comm' {f : β → γ → α} (h : Multipliable (Function.uncurry f)) (h₁ : ∀ b, Multipliable (f b))
(h₂ : ∀ c, Multipliable fun b ↦ f b c) : ∏' (c) (b), f b c = ∏' (b) (c), f b c :=
by
rw [← h.tprod_prod_uncurry h₁, ← h.prod_symm.tprod_prod_uncurry h₂, ← (Equiv.prodComm γ β).tprod_eq (uncurry f)]
rfl
