English
Same as 195435 but stated with minor simplification under regularity assumptions; equality between tprod of f and iterated tprod of fiberwise values.
Русский
То же, что и в 195435, но формулируется с небольшим упрощением под условием регулярности; равенство между т-продуктом f и вложенными т-продуктами по волокнам.
LaTeX
$$$(ha : Multipliable f) → (∀ b, Multipliable (λ c, f ⟨b,c⟩)) → Eq (tprod f) (tprod (λ b, tprod (λ c, f ⟨b,c⟩)))$$$
Lean4
@[to_additive]
protected theorem tprod_sigma' {γ : β → Type*} {f : (Σ b : β, γ b) → α} (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩)
(h₂ : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
(h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm