English
If ha: HasStrictFDerivAt a a' x and hb: HasStrictFDerivAt b b' x, then HasStrictFDerivAt (y ↦ a(y) * b(y)) with derivative a x • b' + a' • b x.
Русский
Если ha: HasStrictFDerivAt a a' x и hb: HasStrictFDerivAt b b' x, тогда HasStrictFDerivAt (y ↦ a(y) * b(y)) имеет производную a x • b' + a' • b x.
LaTeX
$$$\text{HasStrictFDerivAt}\ a\ a'\ x \rightarrow \text{HasStrictFDerivAt}\ b\ b'\ x \rightarrow \text{HasStrictFDerivAt}\ (a(y) \cdot b(y))\ (a x \cdot b' + a' \lhd b x)\ x$$$
Lean4
@[fun_prop]
theorem mul' {x : E} (ha : HasStrictFDerivAt a a' x) (hb : HasStrictFDerivAt b b' x) :
HasStrictFDerivAt (a * b) (a x • b' + a' <• b x) x :=
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasStrictFDerivAt (a x, b x)).comp x (ha.prodMk hb)
