comp_hasStrictFDerivAt_of_eq — Mathlib

English

If hy: y = f x and HasStrictDerivAt h₂ h₂' y, and f has strict Frechet derivative f' at x, then HasStrictFDerivAt (h₂ ∘ f) (h₂' · f') x.

Русский

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

LaTeX

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

Lean4

theorem comp_hasStrictFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) (hh : HasStrictDerivAt h₂ h₂' y)
    (hf : HasStrictFDerivAt f f' x) (hy : y = f x) : HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x := by rw [hy] at hh;
  exact hh.comp_hasStrictFDerivAt x hf

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