English
If c is differentiable within s at x and u is differentiable within s at x, then the product y ↦ (c(y))(u(y)) is differentiable within s at x.
Русский
Если c дифференцируема внутри s в x и u дифференцируема внутри s в x, то y ↦ c(y)(u(y)) дифференциируема внутри s в x.
LaTeX
$$$ \operatorname{DifferentiableWithinAt}_{\mathbb{K}} c s x \land \operatorname{DifferentiableWithinAt}_{\mathbb{K}} u s x \Rightarrow \operatorname{DifferentiableWithinAt}_{\mathbb{K}}\bigl( y \mapsto (c(y))(u(y)) \bigr) s x$$$
Lean4
@[fun_prop]
theorem clm_apply (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
DifferentiableWithinAt 𝕜 (fun y => (c y) (u y)) s x :=
(hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).differentiableWithinAt
