English
If f is an open partial homeomorphism with an invertible derivative at a, then the inverse f.symm has derivative the inverse of f'.
Русский
Если f имеет обратимую производную в точке, то обратная f.symm имеет производную, равную обратной производной f'.
LaTeX
$$$$ \\text{HasStrictFDerivAt } f.symm \\ f'^{-1} \\ a $$$$
Lean4
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` in the sense of strict differentiability at `f.symm a`, then `f.symm` 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 hasStrictFDerivAt_symm (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
(htff' : HasStrictFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) : HasStrictFDerivAt f.symm (f'.symm : F →L[𝕜] E) a :=
htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)
