comp_hasFDerivAtFilter_of_eq — Mathlib

English

If hy: y = f(x) and HasFDerivAt f f' x, then HasFDerivAt (h₂ ∘ f) (h₂' · f') x when h₂ has derivative h₂' at y.

Русский

Если y = f(x) и HasFDerivAt f f' x, то HasFDerivAt (h₂ ∘ f) (h₂' · f') x при условии, что у h₂ есть производная h₂' в y.

LaTeX

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

Lean4

theorem comp_hasFDerivAtFilter_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
    (hh₂ : HasDerivAtFilter h₂ h₂' y L') (hf : HasFDerivAtFilter f f' x L'') (hL : Tendsto f L'' L') (hy : y = f x) :
    HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L'' := by rw [hy] at hh₂; exact hh₂.comp_hasFDerivAtFilter x hf hL

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