Theorems · Theorem · real analysis

contDiff_succ_iff_fderiv

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞},
  ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOnNhd 𝕜 f Set.univ) ∧ ContDiff 𝕜 n (fderiv 𝕜 f)

A function is C^(n + 1) if and only if it is differentiable, and its derivative (formulated in terms of fderiv) is C^n.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Defs

Cited by

4 results in Mathlib

Foundations

Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace