contDiff_succ_iff_deriv — Mathlib

English

On a domain, differentiability implies ContDiff of its derivative.

Русский

На области дифференцируемость порождает ContDiff для производной.

LaTeX

$$$ContDiffOn\ 𝕜\ n\ f\ s \land IsOpen s \Rightarrow ContDiffOn\ 𝕜\ n\ (deriv f)\ s$$$

Lean4

/-- A function is `C^(n + 1)` if and only if it is differentiable,
  and its derivative (formulated in terms of `deriv`) is `C^n`. -/
theorem contDiff_succ_iff_deriv :
    ContDiff 𝕜 (n + 1) f₂ ↔ Differentiable 𝕜 f₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 n (deriv f₂) := by
  simp only [← contDiffOn_univ, contDiffOn_succ_iff_deriv_of_isOpen, isOpen_univ, differentiableOn_univ]

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