English
If c and u have Fréchet derivatives within s at x, then the map y ↦ (c(y))(u(y)) has a Fréchet derivative within s at x, given by the same left-right composition rule as above.
Русский
Если c и u имеют производную Фрéш внутри s в x, то y ↦ c(y)(u(y)) имеет внутри s производную в x, заданную тем же правилом композиции слева и справа, что и выше.
LaTeX
$$$ HasFDerivWithinAt\left( y \mapsto (c(y))(u(y)) \right)\ s\ x = ( (c x)\circ u') + (c'\flip)(u x) $$$
Lean4
@[fun_prop]
theorem clm_apply (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) :
HasFDerivWithinAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x := by
-- `by exact` to solve unification issues.
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x)).comp_hasFDerivWithinAt x (hc.prodMk hu)
