English
Let c be differentiable within s at x and u differentiable within s at x; then the map y ↦ (c(y))(u(y)) is differentiable within s at x with the derivative given by the usual product rule for CLM.
Русский
Пусть c дифференцируема внутри s в x, а u дифференцируема внутри s в x; тогда y ↦ c(y)(u(y)) дифференцируема внутри s в x, производная задаётся правилом произведения для CLM.
LaTeX
$$$ \operatorname{clm\_apply}(hc, hu): \operatorname{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 : DifferentiableOn 𝕜 c s) (hu : DifferentiableOn 𝕜 u s) :
DifferentiableOn 𝕜 (fun y => (c y) (u y)) s := fun x hx => (hc x hx).clm_apply (hu x hx)
