smul_tendsto_smul_iff — Mathlib

English

For groups γ and action of γ on β, Tendsto (c • m) f (c • g) is equivalent to Tendsto m f g, with simplifications; this is a simp lemma.

Русский

Для группы γ, действующей на β, Tendsto (c • m) f (c • g) эквивалентно Tendsto m f g; это упрощающее лемма.

LaTeX

$$$\\mathrm{Tendsto}(c \\cdot m)\\ f\\ (c \\cdot g) \\iff \\mathrm{Tendsto}(m)\\ f\\ g$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_tendsto_smul_iff [Group γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β} :
    Tendsto (c • m) f (c • g) ↔ Tendsto m f g :=
  Group.isUnit _ |>.smul_tendsto_smul_iff

Похожие утверждения