English
If ha: HasFDerivWithinAt a a' s x and hb: HasFDerivWithinAt b b' s x, then HasFDerivWithinAt (y ↦ a(y) * b(y)) with derivative a x • b' + a' <• b x.
Русский
Если ha: HasFDerivWithinAt a a' s x и hb: HasFDerivWithinAt b b' s x, тогда HasFDerivWithinAt (y ↦ a(y) * b(y)) имеет производную a x • b' + a' <• b x.
LaTeX
$$$\text{HasFDerivWithinAt}\ a\ a'\ s\ x \rightarrow \text{HasFDerivWithinAt}\ b\ b'\ s\ x \rightarrow \text{HasFDerivWithinAt}\ (a(y) \cdot b(y))\ (a x \cdot b' + a' \cdot b x)\ s\ x$$$
Lean4
@[fun_prop]
theorem fun_mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x :=
by
convert hc.mul' hd
ext z
apply mul_comm
