fderiv_smul_const — Mathlib

English

If hc: DifferentiableAt 𝕜 c x, then f: F is differentiable at x for y ↦ c(y) · f with derivative (fderiv 𝕜 c x).smulRight f.

Русский

Если c дифференцируема в x, то y ↦ c(y) · f дифференцируема в x, а её производная равна (fderiv 𝕜 c x).smulRight f.

LaTeX

$$$\DifferentiableAt\ 𝕜\ c\ x \Rightarrow \DifferentiableAt\ 𝕜\ (\\lambda y. c(y) \\cdot f)\ x \\Rightarrow fderiv 𝕜 (\\lambda y. c(y) \\cdot f) x = (fderiv 𝕜 c x).smulRight f$$$

Lean4

theorem fderiv_smul_const (hc : DifferentiableAt 𝕜 c x) (f : F) :
    fderiv 𝕜 (fun y => c y • f) x = (fderiv 𝕜 c x).smulRight f :=
  (hc.hasFDerivAt.smul_const f).fderiv

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