English
Let f: E → F be a C^n homeomorphism such that at every point its derivative is a continuous linear isomorphism. Then the inverse map f^{-1}: F → E is also C^n.
Русский
Пусть f: E → F является биективно непрерывно гладкой функцией в смысле C^n и для каждой точки производная Df(t) является неприводимой линейной эквивалентностью. Тогда обратная функция f^{-1} : F → E также является C^n.
LaTeX
$$$\text{Let } E,F \text{ be normed spaces over } \mathbb{K}. \text{ If } f: E \to F \text{ is a } C^n\text{-diffeomorphism (i.e. a } C^n \text{ homeomorphism) and } Df(a) \text{ is a linear isomorphism for all } a \in E, \text{ then } f^{-1} \in C^n(F,E).$$$
Lean4
/-- If `f` is an `n` times continuously differentiable homeomorphism,
and if the derivative of `f` at each point is a continuous linear equivalence,
then `f.symm` is `n` times continuously differentiable.
This is one of the easy parts of the inverse function theorem: it assumes that we already have
an inverse function. -/
theorem contDiff_symm [CompleteSpace E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F}
(hf₀' : ∀ a, HasFDerivAt f (f₀' a : E →L[𝕜] F) a) (hf : ContDiff 𝕜 n (f : E → F)) : ContDiff 𝕜 n (f.symm : F → E) :=
contDiff_iff_contDiffAt.2 fun x => f.toOpenPartialHomeomorph.contDiffAt_symm (mem_univ x) (hf₀' _) hf.contDiffAt
