clm_apply — Mathlib

English

If c is differentiable at x and u is differentiable at x, then y ↦ c(y)(u(y)) is differentiable at x.

Русский

Если c дифференцируема в x и u дифференцируема в x, то y ↦ c(y)(u(y)) дифференцируема в x.

LaTeX

$$$ \operatorname{Differentiable}_{\mathbb{K}} c x \land \operatorname{Differentiable}_{\mathbb{K}} u x \Rightarrow \operatorname{Differentiable}_{\mathbb{K}}\bigl( y \mapsto (c(y))(u(y)) \bigr) x$$$

Lean4

@[fun_prop]
theorem clm_apply (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
    DifferentiableAt 𝕜 (fun y => (c y) (u y)) x :=
  (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).differentiableAt

Похожие утверждения