English
If f is an open partial homeomorphism and f' is invertible at f.symm a, then the inverse f.symm has derivative f'.symm at a.
Русский
Если f — открытое частичное гомеоморфизм и его производная в точке f.symm a обратима, то у f.symm существует производная f'.symm в a.
LaTeX
$$$$ \\text{HasStrictFDerivAt } f.symm \\ (f'.symm) \\ 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 : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a)
(hf : HasFDerivAt f (f' : E →L[𝕜] F) (g a)) (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) :
HasFDerivAt g (f'.symm : F →L[𝕜] E) a :=
by
simp only [← hasFDerivWithinAt_univ, ← nhdsWithin_univ] at hf hfg ⊢
exact hf.of_local_left_inverse (.inf hg (by simp)) (mem_univ _) hfg
