smul_tendsto_smul_iff₀ — Mathlib

English

If γ is a group with zero and acts on β, then for nonzero c, Tendsto (c • m) f (c • g) iff Tendsto m f g.

Русский

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

LaTeX

$$$\\text{GroupWithZero}(\\gamma) \\Rightarrow (c \\neq 0) \\Rightarrow (\\mathrm{Tendsto}(c \\cdot m)\\ f\\ (c \\cdot g) \\iff \\mathrm{Tendsto}(m)\\ f\\ g)$$$

Lean4

theorem smul_tendsto_smul_iff₀ [GroupWithZero γ] [MulAction γ β] {m : α → β} {c : γ} {f : Filter α} {g : Filter β}
    (hc : c ≠ 0) : Tendsto (c • m) f (c • g) ↔ Tendsto m f g :=
  hc.isUnit.smul_tendsto_smul_iff

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