iteratedFDerivWithin_eq_equiv_comp

English

If f has an invertible strict derivative at a, then the derivative of the local inverse is the inverse derivative.

Русский

Если у f строгая обратимая производная в a, то производная локального обратного равна обратной производной.

LaTeX

$$$ HasStrictFDerivAt\ f f'.toContinuousLinearMap a \Rightarrow HasStrictFDerivAt\ (hf.localInverse f f' a) f'.symm.toContinuousLinearMap (f a) $$$

Lean4

/-- Write the iterated Fréchet derivative as the composition of a continuous linear equiv and the
iterated derivative. -/
theorem iteratedFDerivWithin_eq_equiv_comp :
    iteratedFDerivWithin 𝕜 n f s = ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDerivWithin n f s := by
  rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm, Function.id_comp]

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