English
If f is Multipliable on Σ-bundle β×γ, then the product over fibers yields a Multipliable function of the base: b ↦ ∏' c, f⟨b,c⟩ is Multipliable.
Русский
Если f умножаемо на σ-объединение β×γ, тогда произведение по волокнам образует умножаемую функцию базового пространства: b ↦ ∏' c, f⟨b,c⟩ является умножаемой.
LaTeX
$$$$ \text{If } f: (\Sigma b:β, γ b) \to α \text{ is Multipliable, then } b \mapsto \prod' c, f(⟨b,c⟩) \text{ is Multipliable.} $$$$
Lean4
@[to_additive]
theorem sigma {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
ha.sigma' fun b ↦ ha.sigma_factor b