English
If f is differentiable on s, HasFTaylorSeriesUpToOn n f p s and for all y the map x ↦ fderivWithin f s x y is ContDiffOn 𝕜 n on s, then f is ContDiffOn 𝕜 (n+1) on s.
Русский
Если f дифференцируема на s и существует HadFTaylorSeriesUpToOn n f p s, а для всех y отображение x ↦ fderivWithin f s x y является ContDiffOn 𝕜 n на s, тогда f ∈ ContDiffOn 𝕜 (n+1) на s.
LaTeX
$$$\text{DifferentiableOn } 𝕜 f s \to (h' : n = ω \to AnalyticOn 𝕜 f s) \to (\forall y, ContDiffOn 𝕜 n (\lambda x, fderivWithin 𝕜 f s x y) s) \to ContDiffOn 𝕜 (n + 1) f s$$$
Lean4
theorem contDiffOn_succ_of_fderiv_apply [FiniteDimensional 𝕜 D] (hf : DifferentiableOn 𝕜 f s)
(h'f : n = ω → AnalyticOn 𝕜 f s) (h : ∀ y, ContDiffOn 𝕜 n (fun x => fderivWithin 𝕜 f s x y) s) :
ContDiffOn 𝕜 (n + 1) f s :=
contDiffOn_succ_of_fderivWithin hf h'f <| contDiffOn_clm_apply.mpr h
