Theorems · Definition · real analysis

iteratedDeriv

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} → [inst_1 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → ℕ → (𝕜 → F) → 𝕜 → F

The n-th iterated derivative of a function from 𝕜 to F, as a function from 𝕜 to F.

Defined in

Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Cited by

188 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace