English
Let f be a local diffeomorphism of a nontrivially normed field such that f is n-times continuously differentiable at f^{-1}(a) and its derivative at that point is nonzero. Then f^{-1} is n-times continuously differentiable at a.
Русский
Пусть f — локальная диффеоморфизманормированной поля с тем, что f удовлетворяет условию C^n в окрестности f^{-1}(a) и производная в этой точке не равна нулю. Тогда f^{-1} гладна до уровня C^n в точке a.
LaTeX
$$$\text{Let } f: \mathbb{K} \to \mathbb{K} \text{ be a local homeomorphism. If } f \text{ is } C^n \text{ at } f^{-1}(a) \text{ and } f'(f^{-1}(a)) \neq 0, \text{ then } f^{-1} \text{ is } C^n \text{ at } a.$$$
Lean4
/-- Let `f` be a local homeomorphism of a nontrivially normed field, let `a` be a point in its
target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
`f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.
This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem contDiffAt_symm_deriv [CompleteSpace 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {f₀' a : 𝕜} (h₀ : f₀' ≠ 0)
(ha : a ∈ f.target) (hf₀' : HasDerivAt f f₀' (f.symm a)) (hf : ContDiffAt 𝕜 n f (f.symm a)) :
ContDiffAt 𝕜 n f.symm a :=
f.contDiffAt_symm ha (hf₀'.hasFDerivAt_equiv h₀) hf
