deriv_clm_comp — Mathlib

English

If c and d are differentiable within s, then derivWithin of their composition equals the sum of the two projected derivatives.

Русский

Если c и d дифференцируемы на s, то производная внутри s от их композиции равна сумме двух частичных производных.

LaTeX

$$$derivWithin\\left(y \\mapsto (c(y)\\circ(d(y)))\\right)\\,s\\,x = (derivWithin c\\,s\\,x)\\circ d(x) + c(x)\\circ (derivWithin d\\,s\\,x)$$$

Lean4

theorem deriv_clm_comp (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    deriv (fun y => (c y).comp (d y)) x = (deriv c x).comp (d x) + (c x).comp (deriv d x) :=
  (hc.hasDerivAt.clm_comp hd.hasDerivAt).deriv

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