to_localInverse — Mathlib

English

If a function g satisfies g(f x) = x near a, then g has derivative f'.symm at f(a).

Русский

Если g удовлетворяет g(f x) = x близко к a, то g имеет производную f'.symm в точке f(a).

LaTeX

$$$ HasStrictFDerivAt\ g (f'.symm : F →L[𝕜] E) (f(a)) $$$

Lean4

/-- If `f` has an invertible derivative `f'` at `a` in the sense of strict differentiability `(hf)`,
then the inverse function `hf.localInverse f` has derivative `f'.symm` at `f a`. -/
theorem to_localInverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    HasStrictFDerivAt (hf.localInverse f f' a) (f'.symm : F →L[𝕜] E) (f a) :=
  (hf.toOpenPartialHomeomorph f).hasStrictFDerivAt_symm hf.image_mem_toOpenPartialHomeomorph_target <| by
    simpa [← localInverse_def] using hf

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