sigma — Mathlib

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

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