English
If f has a left inverse g near a with f'(g a) ≠ 0 and f is differentiable in a neighbourhood of g a, then g has derivative f'^{-1} at a.
Русский
Если у f есть локальная левая обратная функция g около a, производная f' в g(a) не равна нулю и f дифференцируема в окрестности g(a), то у g есть производная f'^{-1} в a.
LaTeX
$$$ (hg: \\text{ContinuousAt } g \\, a) \\land (hf: \\ HasDerivAt f f' (g a)) \land (hf': f' \\neq 0) \\land (hfg: \\forall^* y \\in 𝓝 a, f(g y)=y) \\Rightarrow \\mathrm{HasDerivAt } g f'^{-1} a $$$
Lean4
/-- If `f (g y) = y` for `y` in some neighborhood of `a`, `g` is continuous at `a`, and `f` has an
invertible derivative `f'` at `g a` in the strict sense, then `g` has the derivative `f'⁻¹` at `a`
in the strict sense.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an
inverse function. -/
theorem of_local_left_inverse {f g : 𝕜 → 𝕜} {f' a : 𝕜} (hg : ContinuousAt g a) (hf : HasStrictDerivAt f f' (g a))
(hf' : f' ≠ 0) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasStrictDerivAt g f'⁻¹ a :=
(hf.hasStrictFDerivAt_equiv hf').of_local_left_inverse hg hfg
