English
Let α be a topological commutative monoid with continuous multiplication. If f : β × γ → α is Multipliable and for every b ∈ β the fiber map c ↦ f(b, c) is Multipliable, then the total infinite product factorizes as an iterated product: ∏' p, f(p) = ∏' b ∈ β ∏' c ∈ γ, f(b, c).
Русский
Пусть α — топологическое коммутативное моноидо с непрерывным умножением. Пусть f : β × γ → α является умножаемой, и для каждого b ∈ β функция c ↦ f(b, c) тоже умножаема. Тогда бесконечное произведение по всем парам разлагается на итеративное произведение: ∏' p, f(p) = ∏' b ∈ β ∏' c ∈ γ f(b, c).
LaTeX
$$$$ \prod' p, f p = \prod' b \; \prod' c, f (b, c). $$$$
Lean4
@[to_additive Summable.tsum_prod']
protected theorem tprod_prod' {f : β × γ → α} (h : Multipliable f) (h₁ : ∀ b, Multipliable fun c ↦ f (b, c)) :
∏' p, f p = ∏' (b) (c), f (b, c) :=
(h.hasProd.prod_fiberwise fun b ↦ (h₁ b).hasProd).tprod_eq.symm
