comp_mdifferentiableWithinAt_of_eq

English

Under appropriate HasMFDerivWithinAt assumptions for g and f, the composition g∘f has HasMFDerivWithinAt with the expected derivative composition.

Русский

При корректных предпосылках HasMFDerivWithinAt для g и f композиция g∘f имеет HasMFDerivWithinAt с ожидаемой композициями производных.

LaTeX

$$$hg\\,HasMFDerivWithinAt I' I'' g u (f x) g' \\land hf\\,HasMFDerivWithinAt I I' f s x f' \\Rightarrow HasMFDerivWithinAt I I'' (g \\circ f) s x (g' \\circ f')$$$

Lean4

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

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