fderiv_fun_mul — Mathlib

English

If a,b are differentiable within s at x, then fderivWithin 𝕜 (fun y => a(y) b(y)) s x equals a(x) • fderivWithin 𝕜 b s x plus b(x) • fderivWithin 𝕜 a s x.

Русский

Если a,b дифференцируемы внутри s в x, то fderivWithin 𝕜 (λ y, a(y) b(y)) s x равно a(x) • fderivWithin 𝕜 b s x плюс b(x) • fderivWithin 𝕜 a s x.

LaTeX

$$$\\forall hxs hc hd,\\ fderivWithin 𝕜 (y \\mapsto a(y) b(y)) s x = a(x) \\cdot fderivWithin 𝕜 b s x + b(x) \\cdot fderivWithin 𝕜 a s x$$$

Lean4

theorem fderiv_fun_mul (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x :=
  (hc.hasFDerivAt.mul hd.hasFDerivAt).fderiv

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