English
If f is an open partial homeomorphism defined near f.symm a and has a nonzero derivative f' at f.symm a in the strict sense, then the inverse f.symm has derivative f'⁻¹ at a in the strict sense.
Русский
Если f является открытым частичным гомоморфизмом, определённым в окрестности f.symm a, и у f в точке f.symm a есть строгая производная f' ≠ 0, то у f.symm есть строгая производная f'⁻¹ в точке a.
LaTeX
$$$ (ha: a ∈ f.target) \\land (hf': f' ≠ 0) \\land (htff': \\mathrm{HasStrictDerivAt} f f' (f.symm a)) \\Rightarrow \\mathrm{HasStrictDerivAt} f.symm f'^{-1} a $$$
Lean4
/-- If `f` is an open partial homeomorphism defined on a neighbourhood of `f.symm a`, and `f` has a
nonzero 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 hasDerivAt_symm (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜} (ha : a ∈ f.target) (hf' : f' ≠ 0)
(htff' : HasDerivAt f f' (f.symm a)) : HasDerivAt f.symm f'⁻¹ a :=
htff'.of_local_left_inverse (f.symm.continuousAt ha) hf' (f.eventually_right_inverse ha)
