contDiffOn_of_completeSpace — Mathlib

English

If f is analytic on a neighborhood of s and the codomain is complete, then ContDiffOn 𝕜 n f s.

Русский

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

LaTeX

$$$AnalyticOnNhd\\ 𝕜\\ 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 : AnalyticOnNhd 𝕜 f s) : ContDiffOn 𝕜 n f s :=
  h.analyticOn.contDiffOn_of_completeSpace

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