const_mul — Mathlib

English

If f tends to c, then b·f tends to b·c under continuous multiplication.

Русский

Если функция f стремится к c, то b·f стремится к b·c при непрерывном умножении.

LaTeX

$$$\text{Tendsto}(f, l, \ nhds c) \Rightarrow \text{Tendsto}(\lambda k. b \cdot f(k), l, \ nhds (b \cdot c))$$$

Lean4

@[to_additive]
theorem const_mul (b : M) {c : M} {f : α → M} {l : Filter α} (h : Tendsto (fun k : α => f k) l (𝓝 c)) :
    Tendsto (fun k : α => b * f k) l (𝓝 (b * c)) :=
  tendsto_const_nhds.mul h

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