fun_const_smul — Mathlib

English

For any c in R, the derivative within at x of y ↦ c • f(y) equals c • f'(x) when f differentiable at x.

Русский

Для любого константного множителя c в R, производная в x функции y ↦ c • f(y) равна c • f'(x) при дифференцируемости f в x.

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c\\,f(y)\\bigr)\\Big|_{y=x} = c\\,f'(x)$$$

Lean4

nonrec theorem fun_const_smul (c : R) (hf : HasStrictDerivAt f f' x) : HasStrictDerivAt (fun y => c • f y) (c • f') x :=
  by simpa using (hf.const_smul c).hasStrictDerivAt

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