iteratedDerivWithin_eq_equiv_comp

English

Write the iterated derivative within s as the composition of the piFieldEquiv inverse with iteratedFDerivWithin.

Русский

Запишите итеративную производную внутри s как композицию обратной piFieldEquiv с iteratedFDerivWithin.

LaTeX

$$$ iteratedDerivWithin n f s = (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm \circ iteratedFDerivWithin 𝕜 n f s $$$

Lean4

/-- Write the iterated derivative as the composition of a continuous linear equiv and the iterated
Fréchet derivative -/
theorem iteratedDerivWithin_eq_equiv_comp :
    iteratedDerivWithin n f s =
      (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s :=
  by ext x; rfl

Похожие утверждения