comp_of_preimage_mem_nhdsWithin_of_eq

English

If g is MDifferentiableWithinAt on u at f(x) and f is MDifferentiableWithinAt on s at x with h ensuring f⁻¹(u) is nhdsWithin x, then g∘f is MDifferentiableWithinAt on s at x with the composed derivative.

Русский

Если g дифференцируема внутри u в f(x) и f дифференцируема внутри s в x и выполняется условие, что f⁻¹(u) относится к nhdsWithin x, то g∘f дифференцируема внутри s в x с композиционной производной.

LaTeX

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

Lean4

theorem comp_of_preimage_mem_nhdsWithin_of_eq {y : M'} (hg : MDifferentiableWithinAt I' I'' g u y)
    (hf : MDifferentiableWithinAt I I' f s x) (h : f ⁻¹' u ∈ 𝓝[s] x) (hy : f x = y) :
    MDifferentiableWithinAt I I'' (g ∘ f) s x := by subst hy;
  exact MDifferentiableWithinAt.comp_of_preimage_mem_nhdsWithin _ hg hf h

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