contDiffOn — Mathlib

English

If f is analytic on s and s has UniqueDiffOn, then ContDiffOn 𝕜 n f s.

Русский

Если f аналитична на s и s обладает UniqueDiffOn, то ContDiffOn 𝕜 n f s.

LaTeX

$$$AnalyticOn\\ 𝕜\\ f\\ s \\land UniqueDiffOn\\ 𝕜\\ s \\Rightarrow ContDiffOn\\ 𝕜\\ n\\ f\\ s$$$

Lean4

/-- On a set with unique differentiability, an analytic function is automatically `C^ω`, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also `AnalyticOnNhd.contDiffOn_of_completeSpace`. -/
theorem contDiffOn (h : AnalyticOnNhd 𝕜 f s) (hs : UniqueDiffOn 𝕜 s) : ContDiffOn 𝕜 n f s :=
  h.analyticOn.contDiffOn hs

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