English
If f is multipliable and g is a homomorphism into a topological monoid with suitable structure, then applying g to the tprod of f yields the tprod of g∘f.
Русский
Если f мультиплируема и существует гомоморфизм g, переходящий в топологический моноид, то применение g к т-производному f дает т-производное от g∘f.
LaTeX
$$$\text{Multipliable } f L\;\Rightarrow\; \forall G,\; g\;\text{continuous} \Rightarrow g(\prod'_[L] i, f(i)) = \prod'_[L] i, g(f(i))$$$
Lean4
@[to_additive]
protected theorem map [CommMonoid γ] [TopologicalSpace γ] (hf : Multipliable f L) {G} [FunLike G α γ]
[MonoidHomClass G α γ] (g : G) (hg : Continuous g) : Multipliable (g ∘ f) L :=
(hf.hasProd.map g hg).multipliable
