comp_of_eq — Mathlib

English

If g is MDifferentiableAt at f(x) and f is MDifferentiableWithinAt, then g∘f is differentiable within at x with the composed derivative.

Русский

Если g дифференцируема в f(x) и f дифференцируем внутри, то g∘f дифференцируема внутри в x с композиционной производной.

LaTeX

$$$hg\\,MDifferentiableAt I' I'' g (f x) \\; hf\\,MDifferentiableWithinAt I I' f s x \\Rightarrow MDifferentiableWithinAt I I'' (g \\circ f) s x$$$

Lean4

theorem comp_of_eq {y : M'} (hg : MDifferentiableAt I' I'' g y) (hf : MDifferentiableAt I I' f x) (hy : f x = y) :
    MDifferentiableAt I I'' (g ∘ f) x := by subst hy; exact hg.comp _ hf

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