English
Let g, g' be maps with left inverse relation, and continuous g, g'. Then Multipliable (g ∘ f) is equivalent to Multipliable f.
Русский
Пусть существуют отображения g, g' с левой обратной связью; тогда мультиплируемость g∘f равна мультиплируемости f.
LaTeX
$$$\text{Continuous } g,\text{Continuous } g',\; \text{LeftInverse } g'\circ g = \mathrm{id} \Rightarrow \text{Multipliable } (g\circ f) L \iff \text{Multipliable } f L$$$
Lean4
@[to_additive]
protected theorem map_iff_of_leftInverse [CommMonoid γ] [TopologicalSpace γ] {G G'} [FunLike G α γ]
[MonoidHomClass G α γ] [FunLike G' γ α] [MonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous g)
(hg' : Continuous g') (hinv : Function.LeftInverse g' g) : Multipliable (g ∘ f) L ↔ Multipliable f L :=
⟨fun h ↦ by
have := h.map _ hg'
rwa [← Function.comp_assoc, hinv.id] at this, fun h ↦ h.map _ hg⟩
