English
The (n+1)-th iterated derivative within s at x equals the derivative within s of the n-th iterated derivative evaluated at x.
Русский
Переход на следующую ступень: (n+1)-я итеративная производная внутри равна внутри-производной от предыдущей ступени.
LaTeX
$$$\operatorname{iteratedDerivWithin}(n+1)\ f\ s\ x = \operatorname{derivWithin}(\operatorname{iteratedDerivWithin} n f s)\ s\ x$$$
Lean4
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative on sets with unique derivatives. -/
theorem contDiffOn_iff_continuousOn_differentiableOn_deriv {n : ℕ∞} (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 n f s ↔
(∀ m : ℕ, (m : ℕ∞) ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
∀ m : ℕ, (m : ℕ∞) < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s :=
by
simp only [contDiffOn_iff_continuousOn_differentiableOn hs, iteratedFDerivWithin_eq_equiv_comp,
LinearIsometryEquiv.comp_continuousOn_iff, LinearIsometryEquiv.comp_differentiableOn_iff]
