comp_mdifferentiableWithinAt — Mathlib

English

If f(x) = y and g is MDifferentiableAt at y, then g∘f is MDifferentiableAt at x with derivative composition.

Русский

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

LaTeX

$$$f x = y \\Rightarrow MDifferentiableAt I' I'' g y \\Rightarrow MDifferentiableAt I I' f x \\Rightarrow MDifferentiableAt I I'' (g \\circ f) x$$$

Lean4

theorem comp_mdifferentiableWithinAt (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableWithinAt I I' f s x) :
    MDifferentiableWithinAt I I'' (g ∘ f) s x :=
  by
  rw [← mdifferentiableWithinAt_univ] at hg
  exact hg.comp _ hf (by simp)

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