contDiffOn_succ_iff_deriv_of_isOpen

English

If f is C^n on an open set, its derivative is C^{n-1} on that set.

Русский

Если функция C^n на открытом множество, её производная является C^{n-1} на этом множестве.

LaTeX

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

Lean4

/-- A function is `C^(n + 1)` on an open domain if and only if it is
differentiable there, and its derivative (formulated with `deriv`) is `C^n`. -/
theorem contDiffOn_succ_iff_deriv_of_isOpen (hs : IsOpen s₂) :
    ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔
      DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧ ContDiffOn 𝕜 n (deriv f₂) s₂ :=
  by
  rw [contDiffOn_succ_iff_derivWithin hs.uniqueDiffOn]
  exact Iff.rfl.and (Iff.rfl.and (contDiffOn_congr fun _ => derivWithin_of_isOpen hs))

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