English
If HasProd (f ∘ Sum.inl) a and HasProd (f ∘ Sum.inr) b, then HasProd f (a · b).
Русский
Если HasProd (f ∘ Sum.inl) a и HasProd (f ∘ Sum.inr) b, то HasProd f (a b).
LaTeX
$$$\\forall f, a, b,\\ HasProd (f \\circ Sum.inl) a \\land HasProd (f \\circ Sum.inr) b \\Rightarrow HasProd f (a \\cdot b)$$$
Lean4
@[to_additive]
theorem sum {α β M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] {f : α ⊕ β → M} {a b : M}
(h₁ : HasProd (f ∘ Sum.inl) a) (h₂ : HasProd (f ∘ Sum.inr) b) : HasProd f (a * b) :=
by
have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) :=
by
rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
convert (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
ext s
simp
simpa [Tendsto, ← Filter.map_map] using this
