English
If f is an open partial homeomorphism and its derivative is invertible, then its inverse has derivative the inverse derivative.
Русский
Если f — открытое частичное гомеоморфизм и его производная обратима, то у обратной функции есть производная, равная обратной производной.
LaTeX
$$$$ \\text{HasFDerivAt}_{{\\text{symm}}} \\; $$$$
Lean4
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has an
invertible derivative `f'` 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 hasFDerivAt_symm (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target)
(htff' : HasFDerivAt f (f' : E →L[𝕜] F) (f.symm a)) : HasFDerivAt f.symm (f'.symm : F →L[𝕜] E) a :=
htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)
