Theorems · Definition · real analysis

ContDiff

(𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type uF} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → Prop

A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. Contrary to the case of definitions in domains (where derivatives might not be unique) we do not need to localize the definition in space or time. The parameter n belongs to ℕ∞ω (accessible in the ContDiff scope), i.e. it can be a natural number, ∞, or ω. For n = ω, we require the function to be analytic. The precise definition we give (all the derivatives should be analytic) is more involved to work around issues when the space is not complete, but it is equivalent when the space is complete.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Defs

Cited by

352 results in Mathlib

Foundations

Depth 171 from the axioms, rests on 4,268 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace