English
Let p, q : M → F' be mappings such that each has a MF-derivative within a set s at a point z, with derivatives p' and q' respectively. Then the product p q also has an MF-derivative within s at z, given by p(z) q' + q(z) p'.
Русский
Пусть p, q : M → F' и каждую из них обладает MF-деривативом внутри множества s в точке z, с производными p' и q' соответственно. Тогда произведение p q также имеет MF-дериватив внутри s в z, который равен p(z) q' + q(z) p'.
LaTeX
$$$\\forall p,q : M \\to F',\\; \\forall s \\subset M, \\forall z \\in M, \\\\ HasMFDerivWithinAt\\ I\\ 𝓘(𝕜, F')\\ p\\ s\\ z\\ p' \\land\\ HasMFDerivWithinAt\\ I\\ 𝓘(𝕜, F')\\ q\\ s\\ z\\ q' \\Rightarrow \\\\ HasMFDerivWithinAt\\ I\\ 𝓘(𝕜, F')\\ (p \\cdot q)\\ s\\ z\\ (p(z) \\; q' + q(z) \\; p').$$$
Lean4
theorem mul (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p') (hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q') :
HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p' : E →L[𝕜] F') := by convert hp.mul' hq; ext _;
apply mul_comm
