English
The (n+1)-st iterated derivative within a set with unique derivatives can be obtained by differentiating the n-th derivative.
Русский
Положения (n+1)-й итеративной производной внутри множества с уникальными производными получаем дифференцируя n-ю производную.
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_nat_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
rw [show n = ((n : ℕ∞) : WithTop ℕ∞) from rfl, contDiffOn_iff_continuousOn_differentiableOn_deriv hs]
simp
