fderiv_fun_const_smul — Mathlib

English

Differentiating the smoothed function c · f at a point x yields the smoothed derivative: fderiv 𝕜 (λ y, c · f y) x = c · fderiv 𝕜 f x.

Русский

Производная функции y ↦ c · f(y) равна c · производной f: fderiv 𝕜 (λ y, c · f y) x = c · fderiv 𝕜 f x.

LaTeX

$$$ \mathrm{fderiv}_{𝕜} (\lambda y. c \cdot f(y)) \, x = c \cdot \mathrm{fderiv}_{𝕜} f \, x$$$

Lean4

theorem fderiv_fun_const_smul (h : DifferentiableAt 𝕜 f x) (c : R) : fderiv 𝕜 (fun y => c • f y) x = c • fderiv 𝕜 f x :=
  (h.hasFDerivAt.const_smul c).fderiv

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