const_smul — Mathlib

English

If f converges to a under a filter l, then for any fixed scalar c ∈ M, the function x ↦ c • f(x) converges to c • a under l.

Русский

Если f стремится к a по фильтру l, то для любых фиксированных скалярных множителей c ∈ M функция x ↦ c • f(x) стремится к c • a по l.

LaTeX

$$$\text{Tendsto } f\ l\ (\mathcal{N} a) \ \Rightarrow\ \text{Tendsto } (\lambda x. c \cdot f(x))\ l\ (\mathcal{N} (c \cdot a)).$$$

Lean4

@[to_additive]
theorem const_smul {f : β → α} {l : Filter β} {a : α} (hf : Tendsto f l (𝓝 a)) (c : M) :
    Tendsto (fun x => c • f x) l (𝓝 (c • a)) :=
  ((continuous_const_smul _).tendsto _).comp hf

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