English
If c,d are differentiable within s at x, then fderivWithin 𝕜 (c d) s x equals c(x) • fderivWithin d s x + d(x) • fderivWithin c s x.
Русский
Если функции c,d дифференцируемы внутри s в точке x, то производная внутри s от произведения cd равна c(x) fderivWithin d s x плюс d(x) fderivWithin c s x.
LaTeX
$$$\\forall hxs, hc, hd,\\ fderivWithin 𝕜 (c \\cdot d) s x = c(x) \\cdot fderivWithin 𝕜 d s x + d(x) \\cdot fderivWithin 𝕜 c s x$$$
Lean4
theorem fderivWithin_mul (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x) :
fderivWithin 𝕜 (c * d) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x :=
(hc.hasFDerivWithinAt.mul hd.hasFDerivWithinAt).fderivWithin hxs
