English
If hxs, ha, hb hold as in the statement, then fderivWithin (a b) s x equals a(x) • fderivWithin b s x plus fderivWithin a s x acting on b x.
Русский
При выполнении условий hxs, ha, hb формула для fderivWithin произведения: 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_mul' (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x) :
fderivWithin 𝕜 (a * b) s x = a x • fderivWithin 𝕜 b s x + fderivWithin 𝕜 a s x <• b x :=
(ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).fderivWithin hxs
