English
If g is a topological equivalence between α and γ (with a continuous forward map and a continuous inverse), then Multipliable (g ∘ f) L is equivalent to Multipliable f L for any f : β → α and any L.
Русский
Если g задаёт взаимно однозначное непрерывное отображение между au, и его обратное отображение непрерывно, то Multipliable (g ∘ f) L эквивалентно Multipliable f L для любого f : β → α и любого L.
LaTeX
$$Multipliable (Function.comp g f) L ↔ Multipliable f L$$
Lean4
/-- "A special case of `Multipliable.map_iff_of_leftInverse` for convenience" -/
@[to_additive /-- A special case of `Summable.map_iff_of_leftInverse` for convenience -/
]
protected theorem map_iff_of_equiv [CommMonoid γ] [TopologicalSpace γ] {G} [EquivLike G α γ] [MulEquivClass G α γ]
(g : G) (hg : Continuous g) (hg' : Continuous (EquivLike.inv g : γ → α)) :
Multipliable (g ∘ f) L ↔ Multipliable f L :=
Multipliable.map_iff_of_leftInverse g (g : α ≃* γ).symm hg hg' (EquivLike.left_inv g)
