contDiffOn_of_differentiableOn — Mathlib

English

If for every m, m ≤ n, the iterated derivatives iteratedFDerivWithin 𝕜 m f s are differentiable on s, then ContDiffOn 𝕜 (WithTop.some n) f s.

Русский

Если для каждого m ≤ n итеративные производные дифференцируемы на s, то ContDiffOn 𝕜 (WithTop.some n) f s.

LaTeX

$$(∀ m, m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) → ContDiffOn 𝕜 (WithTop.some n) f s$$

Lean4

theorem contDiffOn_of_differentiableOn {n : ℕ∞}
    (h : ∀ m : ℕ, m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s) : ContDiffOn 𝕜 n f s :=
  contDiffOn_of_continuousOn_differentiableOn (fun m hm => (h m hm).continuousOn) fun m hm => h m (le_of_lt hm)

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