English
If hp and hq are MF-derivatives at z of p and q respectively, then the product p q has MF-derivative at z equal to p(z) q' + q(z) p'.
Русский
Если hp и hq являются MF-деривативами в точке z функций p и q соответственно, тогда произведение p q имеет MF-дериватив в z, равный p(z) q' + q(z) p'.
LaTeX
$$$\\forall hp\\, hq:\\ HasMFDerivAt\\ I 𝓘(𝕜, F')\\ p\\ z\\ p'\\;\\ q\\ z\\ q' \\Rightarrow \\\\ HasMFDerivAt\\ I 𝓘(𝕜, F')\\ (p \\cdot q)\\ z\\ (p(z) \\; q' + q(z) \\; p').$$$
Lean4
theorem mul (hp : HasMFDerivAt I 𝓘(𝕜, F') p z p') (hq : HasMFDerivAt I 𝓘(𝕜, F') q z q') :
HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z • q' + q z • p' : E →L[𝕜] F') :=
hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.mul hq.hasMFDerivWithinAt
