contDiffOn_of_completeSpace — Mathlib

English

If f is analytic on s, then ContDiffOn 𝕜 n f s holds for any n, provided the codomain is a complete space.

Русский

Если f аналитична на s, тогда ContDiffOn 𝕜 n f s верно для любого n при условии полноты пространства-куба.

LaTeX

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

Lean4

/-- An analytic function is automatically `C^ω` in a complete space -/
theorem contDiffOn_of_completeSpace [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : ContDiffOn 𝕜 n f s := fun x hx ↦
  (h x hx).contDiffWithinAt

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