English
If f has a left inverse g near a with f' ≠ 0 and f(g(y))=y near a, then g has derivative f'⁻¹ at a.
Русский
Если у f есть локальная левая обратная функция g около a, производная f' не равна нулю, и f(g(y))=y около a, то g имеет производную f'⁻¹ в a.
LaTeX
$$$ (hg: \\text{ContinuousAt } g \\, a) \\land (hf: \\mathrm{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`, then `g` has the derivative `f'⁻¹` at `a`.
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 : HasDerivAt f f' (g a))
(hf' : f' ≠ 0) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasDerivAt g f'⁻¹ a :=
(hf.hasFDerivAt_equiv hf').of_local_left_inverse hg hfg
