comp — Mathlib

English

If B is a bilinear map and f,g differentiable with derivatives at x, then the derivative of y ↦ B(f(y), g(y)) at x is given by the sum of two precomposition terms.

Русский

Если B — билинейное отображение и f,g дифференцируемы в x, то производная y ↦ B(f(y), g(y)) в x равна сумме двух предобразов.

LaTeX

$$$\text{HasFDerivAt} (y\mapsto B(f(y), g(y))) x = B.precompR(G')(f x) g' + B.precompL G' f' (g x)$$$

Lean4

/-- The chain rule. -/
@[fun_prop]
theorem comp {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) :
    HasFDerivAt (g ∘ f) (g'.comp f') x :=
  HasFDerivAtFilter.comp x hg hf hf.continuousAt

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