English
If c differentiable at x with derivative c' and u differentiable at x with derivative u', then the differential of y ↦ (c(y))(u(y)) at x is the sum of the left and right contributions described by compL.
Русский
Если c дифференцируема в x с производной c' и u дифференцируема в x с производной u', то дифференциал f(y) = c(y)(u(y)) в x равен сумме левых и правых вкладов через compL.
LaTeX
$$$ f'(x) = (c(x) \circ u') + (c'\mathrm{flip})(u(x)) $$$
Lean4
theorem fderivWithin_clm_apply (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x)
(hu : DifferentiableWithinAt 𝕜 u s x) :
fderivWithin 𝕜 (fun y => (c y) (u y)) s x = (c x).comp (fderivWithin 𝕜 u s x) + (fderivWithin 𝕜 c s x).flip (u x) :=
(hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).fderivWithin hxs
