English
Inverse of a smooth, nondegenerate homeomorphism is also smooth.
Русский
Обратная функция гладкого гомеоморфа также гладкая.
LaTeX
$$$\text{contDiff_symm_deriv} \; [CompleteSpace 𝕜] \ (f : 𝕜 \simeq 𝕜) \to (\forall x, f'(x) \neq 0) \to (\forall x, HasDerivAt f (f'(x)) x) \to ContDiff 𝕜 n (f^{-1})$$$
Lean4
/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nontrivially normed
field. Suppose that the derivative of `f` is never equal to zero. 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_deriv [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜} (h₀ : ∀ x, f' x ≠ 0)
(hf' : ∀ x, HasDerivAt f (f' x) x) (hf : ContDiff 𝕜 n (f : 𝕜 → 𝕜)) : ContDiff 𝕜 n (f.symm : 𝕜 → 𝕜) :=
contDiff_iff_contDiffAt.2 fun x =>
f.toOpenPartialHomeomorph.contDiffAt_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.contDiffAt
