comp_of_eq — Mathlib

English

If g is MDifferentiableWithinAt and f is MDifferentiableWithinAt, then g∘f is MDifferentiableWithinAt with the appropriate derivative composition.

Русский

Если g дифференцируема внутри и f дифференцируема внутри, то g∘f дифференцируема внутри с составлением производных.

LaTeX

$$$HasMDifferentiableWithinAt I' I'' g u (f x) \\; g'\\ \\land\\ HasMDifferentiableWithinAt I I' f s x \\Rightarrow HasMDifferentiableWithinAt I I'' (g \\circ f) s x$$$

Lean4

theorem comp_of_eq {y : M'} (hg : MDifferentiableWithinAt I' I'' g u y) (hf : MDifferentiableWithinAt I I' f s x)
    (h : s ⊆ f ⁻¹' u) (hy : f x = y) : MDifferentiableWithinAt I I'' (g ∘ f) s x := by subst hy; exact hg.comp _ hf h

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