English
For any group G acting on α with continuous constant smul, Tendsto (c • f) to nhds (c • a) is equivalent to Tendsto f to nhds a.
Русский
При действии группы G на α непрерывным константным смулом выполняется равносильность: Tendsto (c•f) к nhds (c•a) эквивалентно Tendsto f к nhds a.
LaTeX
$$$ \\operatorname{Tendsto}(\\lambda x. c \\cdot f\\,x)\\;l\\; (\\mathcal{nhds}(c \\cdot a)) \\ \\Leftrightarrow \\ \\operatorname{Tendsto}(\\lambda x. f\\,x)\\;l\\; (\\mathcal{nhds}(a)) $$$
Lean4
@[to_additive]
theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G) :
Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩
