English
Let c be a unit in the monoid γ. Then Tendsto (c • m) f (c • g) is equivalent to Tendsto m f g; the invertibility of c allows reversal of the smul.
Русский
Пусть c является единицей (обратимым элементом) в моноиде γ. Тогда Tendsto (c • m) f (c • g) эквивалентно Tendsto m f g; обратимость c позволяет обратить смул.
LaTeX
$$$\\text{IsUnit}(c) \\Rightarrow \\mathrm{Tendsto}(c \\cdot m)\\ f\\ (c \\cdot g) \\iff \\mathrm{Tendsto}(m)\\ f\\ g$$$
Lean4
@[to_additive]
theorem _root_.IsUnit.smul_tendsto_smul_iff [Monoid γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β}
(hc : IsUnit c) : Tendsto (c • m) f (c • g) ↔ Tendsto m f g :=
by
rcases hc.exists_left_inv with ⟨d, hd⟩
refine ⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩
simpa [Function.comp_def, smul_smul, hd] using (tendsto_map (f := (d • ·))).comp H
