English
The (n+1)-st iterated derivative is the composition of a curry-right equiv with the n-th derivative of f's derivative.
Русский
(n+1)-я итеративная производная есть композиция карри-правого эквивалента с n-й производной производной f.
LaTeX
$$$\operatorname{iteratedFDeriv}_{\mathbb{k}}(n+1)\ f\ x =\big(\text{continuousMultilinearCurryRightEquiv'}_{\mathbb{k}}\ n\ E\ F\big)^{\mathrm{symm}}\circ \operatorname{iteratedFDeriv}_{\mathbb{k}} n (\lambda y.\ fderiv_{\mathbb{k}} f\ y)\ x$$$
Lean4
theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f :=
by
ext1 x; ext1 n
change iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x
rw [iteratedFDerivWithin_univ]