English
Let s have unique differentiability. Then ContDiffOn 𝕜 n f s is equivalent to: for all m in natural numbers with m ≤ n, the m-th iterated derivative within s is continuous on s, and for all m with m < n the m-th iterated derivative within s is differentiable on s.
Русский
Пусть s имеет уникальные производные. Тогда ContDiffOn 𝕜 n f s эквивалентно: для всех m∈ℕ, если m≤n, то m-я повторная производная внутри s непрерывна на s, и для всех m<m значение m-й повторной производной внутри s дифференцируемо на s.
LaTeX
$$$\\text{UniqueDiffOn } 𝕜\, s \\Rightarrow \\ContDiffOn 𝕜 n f s \\iff (\\forall m : \\mathbb{N},\\ m \\le n \\to \\operatorname{ContinuousOn}(\\lambda x. \\operatorname{iteratedFDerivWithin} 𝕜 m f s x)\\, s) \\land (\\forall m : \\mathbb{N},\\ m < n \\to \\operatorname{DifferentiableOn} 𝕜 (\\lambda x. \\operatorname{iteratedFDerivWithin} 𝕜 m f s x) \\; s)$$
Lean4
theorem contDiffOn_nat_iff_continuousOn_differentiableOn {n : ℕ} (hs : UniqueDiffOn 𝕜 s) :
ContDiffOn 𝕜 n f s ↔
(∀ m : ℕ, m ≤ n → ContinuousOn (fun x => iteratedFDerivWithin 𝕜 m f s x) s) ∧
∀ m : ℕ, m < n → DifferentiableOn 𝕜 (fun x => iteratedFDerivWithin 𝕜 m f s x) s :=
by
rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]
simp
