English
Let a,b be differentiable within s at x. Then fderivWithin (a b) s x = a(x) • fderivWithin b s x + fderivWithin a s x <• b x.
Русский
Пусть a,b дифференцируемы внутри s в точке x. Тогда fderivWithin (a b) s x = a(x) • fderivWithin b s x + fderivWithin a s x <• b x.
LaTeX
$$$\\forall hxs ha hb,\\ fderivWithin 𝕜 (a \\cdot b) s x = a(x) \\cdot fderivWithin 𝕜 b s x + fderivWithin 𝕜 a s x <• b(x)$$$
Lean4
theorem fderivWithin_fun_mul (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x) :
fderivWithin 𝕜 (fun y => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x :=
(hc.hasFDerivWithinAt.mul hd.hasFDerivWithinAt).fderivWithin hxs
