English
Under the same hypotheses as above, the i-th iterated derivative within s satisfies the same Taylor composition equality.
Русский
При тех же условиях справедливо то же равенство для i-й итеративной производной внутри s.
LaTeX
$$$\forall i,\; \operatorname{iteratedFDerivWithin} 𝕜 i (g \circ f) s x = (\ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (\ftaylorSeriesWithin 𝕜 f s x) i$$$
Lean4
theorem comp_contDiffWithinAt {g : F → G} {f : E → F} (h : ContDiff 𝕜 n g) (hf : ContDiffWithinAt 𝕜 n f t x) :
ContDiffWithinAt 𝕜 n (g ∘ f) t x :=
haveI : ContDiffWithinAt 𝕜 n g univ (f x) := h.contDiffAt.contDiffWithinAt
this.comp x hf (subset_univ _)