English
If g is C^n at y and f is C^n within s at x with f(x) = y, then the composition g ∘ f is C^n within s at x.
Русский
Если g имеет класс C^n в точке y и f имеет класс C^n внутри s в точке x с условием f(x)=y, то композиция g ∘ f имеет C^n внутри s в x.
LaTeX
$$$\forall x\in E,\; \ContDiffAt 𝕜 n g y\rightarrow \ContDiffWithinAt 𝕜 n f s x\rightarrow f x = y\rightarrow \ContDiffWithinAt 𝕜 n (g \circ f) s x$$$
Lean4
theorem iteratedFDerivWithin_comp {t : Set F} (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hst : MapsTo f s t) {i : ℕ} (hi : i ≤ n) :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
(ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i :=
iteratedFDerivWithin_comp_of_eventually_mem hg hf ht hs hx (eventually_mem_nhdsWithin.mono hst) hi
