to_localInverse — Mathlib

English

There is a local inverse g with derivative f'^{-1} at f a.

Русский

Существует локальная обратная g с производной f'^{-1} в точке f a.

LaTeX

$$$\text{HasStrictDerivAt } f f' a \Rightarrow \text{HasStrictDerivAt } (\text{HasStrictDerivAt.localInverse } f f' a) f'^{-1} (f a)$$$

Lean4

theorem to_localInverse : HasStrictDerivAt (hf.localInverse f f' a hf') f'⁻¹ (f a) :=
  (hf.hasStrictFDerivAt_equiv hf').to_localInverse

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