continuousOn_iteratedFDerivWithin

English

If f is analytic on s, then ContDiffOn 𝕜 n f s for all n in a complete space.

Русский

Если f аналитична на s, то ContDiffOn 𝕜 n f s для всех n в полном пространстве.

LaTeX

$$$AnalyticOn\\ 𝕜\\ f\\ s \\rightarrow ContDiffOn\\ 𝕜\\ n\\ f\\ s$$$

Lean4

theorem continuousOn_iteratedFDerivWithin {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : m ≤ n) (hs : UniqueDiffOn 𝕜 s) :
    ContinuousOn (iteratedFDerivWithin 𝕜 m f s) s :=
  ((h.of_le hmn).ftaylorSeriesWithin hs).cont m le_rfl

Похожие утверждения