English
Writing the (n+1)-st iterated differential as the composition of a currying right equivalence with the n-th derivative of the derivative, one obtains an explicit equality that identifies the (n+1)-st derivative with the appropriate currying of the n-th derivative of the derivative.
Русский
Записывая (n+1)-ю повторную дифференциал через композицию правого эквивалента курации с n-й производной от производной, получаем точное тождество, идентифицирующее (n+1)-ю производную с соответствующим кураванием n-й производной от производной.
LaTeX
$$$\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(n+1)} f\,s\,x = \big( (\text{continuousMultilinearCurryRightEquiv}' \,\mathbb{K}\, n \; E \; F)^{\!s} \circ \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n} ( fderivWithin_{\mathbb{K}} f \; s \; y ) \; s \big) x$$$
Lean4
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative. -/
theorem iteratedFDerivWithin_succ_eq_comp_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
iteratedFDerivWithin 𝕜 (n + 1) f s x =
((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
x :=
by ext m; simp [iteratedFDerivWithin_succ_apply_right hs hx]
