contDiffOn_infty_iff_derivWithin — Mathlib

English

On an open set, C^{n+1} is equivalent to differentiability and the derivative is C^n.

Русский

На открытой области C^{n+1} эквивалентна дифференцируемости и тому, что производная является C^n.

LaTeX

$$$ContDiffOn\ 𝕜\ (n+1) f\ s \iff\ DifferentiableOn 𝕜 f\ s \land (n=ω \rightarrow AnalyticOn 𝕜 f\ s) \land ContDiffOn 𝕜\ n (derivWithin f\ s)\ s$$

Lean4

theorem contDiffOn_infty_iff_derivWithin (hs : UniqueDiffOn 𝕜 s₂) :
    ContDiffOn 𝕜 ∞ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ∞ (derivWithin f₂ s₂) s₂ :=
  by
  rw [show ∞ = ∞ + 1 by rfl, contDiffOn_succ_iff_derivWithin hs]
  simp

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