Theorems · Theorem · global analysis

HasFDerivAt.comp_semilinear

∀ {𝕜 : Type u_1} {V : Type u_2} {V' : Type u_3} {W : Type u_4} {W' : Type u_5} [inst : NontriviallyNormedField 𝕜]
  {σ σ' : 𝕜 →+* 𝕜} [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup V']
  [inst_4 : NormedSpace 𝕜 V'] [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W]
  [inst_7 : NormedAddCommGroup W'] [inst_8 : NormedSpace 𝕜 W'] [RingHomIsometric σ] [inst_10 : RingHomInvPair σ σ']
  (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {z : V'} {f' : V →L[𝕜] W},
  HasFDerivAt f f' (R z) → HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) z

If L and R are semilinear maps whose composite is linear, and f has Fréchet derivative f' at R z, then L ∘ f ∘ R has Fréchet derivative L ∘ f' ∘ R at z.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceRingHomIsometricRingHomInvPair