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' (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :
HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a' <• b x) s x := by
-- `by exact` to solve unification issues.
exact
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt (a x, b x)).comp_hasFDerivWithinAt x (ha.prodMk hb)
