comp_hasFDerivAt — Mathlib

English

If hy: y = f x and HasStrictDerivAt h₂ h₂' y, then HasFDerivAt (h₂ ∘ f) (h₂' · f') x.

Русский

Если y = f x и HasStrictDerivAt h₂ h₂' y, то HasFDerivAt (h₂ ∘ f) (h₂' · f') x.

LaTeX

$$$\text{If } y = f x \text{ and } HasStrictDerivAt h_2 h_2' y, \text{ then } HasFDerivAt (h_2 \circ f) (h_2' \cdot f') x.$$$

Lean4

theorem comp_hasFDerivAt {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasDerivAt h₂ h₂' (f x)) (hf : HasFDerivAt f f' x) :
    HasFDerivAt (h₂ ∘ f) (h₂' • f') x :=
  hh.comp_hasFDerivAtFilter x hf hf.continuousAt

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