Theorems · Theorem · global analysis

fderivWithin_fderivWithin

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {x : E} {y : F} {s : Set E}
  {t : Set F},
  DifferentiableWithinAt 𝕜 g t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          f x = y → ∀ (v : E), (fderivWithin 𝕜 g t y) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) v

A version of fderivWithin_comp that is useful to rewrite the composition of two derivatives into a single derivative. This version always applies, but creates a new side-goal f x = y.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Comp

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace