English
Let G, G' be monoid-like structures with maps g and g' such that g' is left inverse of g (i.e., g' ∘ g = id). Then Multipliable f with respect to the composition g ∘ f is equivalent to Multipliable f.
Русский
Пусть существуют отображения g и g' между моноидами с g' слева от g (g' ∘ g = id). Тогда мультиплируемость f относительно составной функции g ∘ f эквивалентна мультиплируемости f.
LaTeX
$$$\text{Continuous maps and left-inverse condition }(g'∘g=\mathrm{id})\;\Rightarrow\; \text{Multipliable } (g\circ f) L \iff \text{Multipliable } f L$$$
Lean4
@[to_additive]
protected theorem map [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a L) {G} [FunLike G α γ]
[MonoidHomClass G α γ] (g : G) (hg : Continuous g) : HasProd (g ∘ f) (g a) L :=
by
have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b := funext <| map_prod g _
unfold HasProd
rw [← this]
exact (hg.tendsto a).comp hf
