English
If c,d are differentiable within s at x, then fderivWithin 𝕜 (fun y => c(y) d(y)) s x equals c(x) • fderivWithin d s x plus d(x) • fderivWithin c s x.
Русский
Если функции c,d дифференцируемы внутри s в x, то fderivWithin 𝕜 (λ y, c(y) d(y)) s x равняется c(x) • fderivWithin d s x плюс d(x) • fderivWithin c s x.
LaTeX
$$$\\forall hxs, hc, hd,\\ fderivWithin 𝕜 (y \\mapsto c(y) d(y)) s x = c(x) \\cdot fderivWithin 𝕜 d s x + d(x) \\cdot fderivWithin 𝕜 c s x$$$
Lean4
theorem fderiv_fun_mul' (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :
fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + fderiv 𝕜 a x <• b x :=
(ha.hasFDerivAt.mul' hb.hasFDerivAt).fderiv
