English
Under the stated hypotheses, the same equality for tprod holds: the g-image of the tprod equals the tprod of the mapped function.
Русский
При данных гипотезах выполняется то же равенство для т-производного: образ по g т-pроизводного равен т-производному от отображения.
LaTeX
$$$\text{Multipliable } f L \Rightarrow \forall g\ (\text{Continuous } g) \Rightarrow g(\operatorname{tprod} f L) = \operatorname{tprod} (g\circ f) L$$$
Lean4
@[to_additive]
theorem map_tprod [L.NeBot] [CommMonoid γ] [TopologicalSpace γ] [T2Space γ] (hf : Multipliable f L) {G} [FunLike G α γ]
[MonoidHomClass G α γ] (g : G) (hg : Continuous g) : g (∏'[L] i, f i) = ∏'[L] i, g (f i) :=
(HasProd.tprod_eq (HasProd.map hf.hasProd g hg)).symm
