fun_const_smul — Mathlib

English

If f has a strict derivative at x, then multiplying f by a constant scalar c yields a function whose derivative is the constant multiple c·f'.

Русский

Если у функции f в точке x существует строгая производная, то умножение f на константу c дает производную, равную c·f'.

LaTeX

$$$ h : HasStrictFDerivAt f f' x \\implies \\forall c, HasStrictFDerivAt (c \\cdot f) (c \\cdot f') x $$$

Lean4

@[fun_prop]
theorem fun_const_smul (h : HasStrictFDerivAt f f' x) (c : R) : HasStrictFDerivAt (fun x => c • f x) (c • f') x :=
  (c • (1 : F →L[𝕜] F)).hasStrictFDerivAt.comp x h

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