Theorems · Definition · real analysis

ContDiffOn

(𝕜 : 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) → Set E → Prop

A function is continuously differentiable up to n on s if, for any point x in s, it admits continuous derivatives up to order n on a neighborhood of x in s. The parameter n belongs to ℕ∞ω (accessible in the ContDiff scope), i.e. it can be a natural number, ∞, or ω. For n = ∞, we only require that this holds up to any finite order (where the neighborhood may depend on the finite order we consider). For n = ω, we require the function to be analytic within s at every point of s. 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

294 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace