tendsto_const_smul_iff — Mathlib

English

If c is a unit, Tendsto (λ x, c • f x) l (nhds (c • a)) is equivalent to Tendsto f l (nhds a).

Русский

Пусть c единица. Тогда сходимость x ↦ c • f x в l в окрестности c • a эквивалентна сходимости f в l в окрестности a.

LaTeX

$$$\text{Tendsto} (\lambda x \mapsto c \cdot f x)\ l\ (nhds (c \cdot a)) \ \iff \ \text{Tendsto} f\ l\ (nhds a)$$$

Lean4

nonrec theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} {c : M} (hc : IsUnit c) :
    Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
  tendsto_const_smul_iff hc.unit

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