continuousOn_fderiv_of_isOpen — Mathlib

English

If f is analytic on s and fderivWithin is ContDiffOn ω on s, then f is ContDiffOn (ω+1) on s.

Русский

Если f аналитична на s и fderivWithin 𝕜 f s ∈ ContDiffOn ω на s, то f ∈ ContDiffOn (ω+1) на s.

LaTeX

$$$\\text{AnalyticOn } 𝕜 f s \\land \\ContDiffOn 𝕜 ω (fderivWithin 𝕜 f s) s \\Rightarrow \\ContDiffOn 𝕜 (ω+1) f s$$$

Lean4

theorem continuousOn_fderiv_of_isOpen (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hn : 1 ≤ n) :
    ContinuousOn (fderiv 𝕜 f) s :=
  ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 (h.of_le (show 0 + (1 : WithTop ℕ∞) ≤ n from hn))).2.2.continuousOn

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