comp_of_preimage_mem_nhdsWithin — Mathlib

English

If f x = y and g is differentiable at y, then g∘f is differentiable at x with derivative equal to the composition of the derivatives.

Русский

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

LaTeX

$$$f x = y\\Rightarrow MDifferentiableWithinAt I' I'' g u y \\Rightarrow MDifferentiableWithinAt I I' f s x \\Rightarrow MDifferentiableWithinAt I I'' (g \\circ f) s x$$$

Lean4

theorem comp_of_preimage_mem_nhdsWithin (hg : MDifferentiableWithinAt I' I'' g u (f x))
    (hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x) : MDifferentiableWithinAt I I'' (g ∘ f) s x :=
  (hg.comp _ (hf.mono inter_subset_right) inter_subset_left).mono_of_mem_nhdsWithin
    (Filter.inter_mem h self_mem_nhdsWithin)

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