fderiv_comp_deriv_of_eq — Mathlib

English

If l differentiableWithinAt t, f differentiableWithinAt s, and hy describes equality, then the derivative of l ∘ f equals the applied Fréchet derivative to the derivative inside s.

Русский

Если l дифференцируемо внутри t, f внутри s, и есть равенство, то производная l∘f равна применённой фреше-деривативе к производной.

LaTeX

$$$$fderivWithin\ 𝕜 l t (f x) \land derivWithin (l \circ f) s x = (fderivWithin 𝕜 l t (f x) : F \to E) (derivWithin f s x)$$$$

Lean4

theorem fderiv_comp_deriv_of_eq (hl : DifferentiableAt 𝕜 l y) (hf : DifferentiableAt 𝕜 f x) (hy : y = f x) :
    deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x) := by rw [hy] at hl; exact fderiv_comp_deriv x hl hf

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