English
If HasProd g a and HasProd (λ b, λ c, f ⟨b,c⟩) (g b) and f is Multipliable, then HasProd f a.
Русский
Если HasProd g a и HasProd (λ b, λ c, f ⟨b,c⟩) (g b) и f выполнима в виде Multipliable, тогда HasProd f a.
LaTeX
$$$ HasProd g a \\land (\\forall b, HasProd (λ c, f ⟨b,c⟩) (g b)) \\Rightarrow HasProd f a$$$
Lean4
/-- If a function `f` on `β × γ` has product `a` and for each `b` the restriction of `f` to
`{b} × γ` has product `g b`, then the function `g` has product `a`. -/
@[to_additive HasSum.prod_fiberwise /-- If a series `f` on `β × γ` has sum `a` and for each `b` the
restriction of `f` to `{b} × γ` has sum `g b`, then the series `g` has sum `a`. -/
]
theorem prod_fiberwise {f : β × γ → α} {g : β → α} {a : α} (ha : HasProd f a)
(hf : ∀ b, HasProd (fun c ↦ f (b, c)) (g b)) : HasProd g a :=
HasProd.sigma ((Equiv.sigmaEquivProd β γ).hasProd_iff.2 ha) hf
