comp_hasFDerivWithinAt — Mathlib

English

If HasFDerivWithinAt for g at f(x) and HasFDerivWithinAt for f at x hold, then HasFDerivWithinAt for the composition g ∘ f holds within the same set with a derivative given by the bilinear composition formula.

Русский

Если существуют внутри-дифференцирования для g в f(x) и для f в x, то существует внутри-дифференцирование композиции g∘f с производной как сумма двух предмножителей билинейного отображения.

LaTeX

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

Lean4

@[fun_prop]
theorem comp_hasFDerivWithinAt {g : F → G} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x))
    (hf : HasFDerivWithinAt f f' s x) : HasFDerivWithinAt (g ∘ f) (g'.comp f') s x :=
  hg.comp x hf hf.continuousWithinAt

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