Theorems · Theorem · real analysis

iteratedDerivWithin_sum

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_7} {n : ℕ} {x : 𝕜} {f : ι → 𝕜 → F} {I : Finset ι} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      (∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n) (f i) s x) →
        iteratedDerivWithin n (∑ i ∈ I, f i) s x = ∑ i ∈ I, iteratedDerivWithin n (f i) s x

Defined in

Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace