ContDiffAt.to_localInverse

theorem ContDiffAt.to_localInverse : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕂 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕂 F] [inst_5 : CompleteSpace E] {f : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 ≤ n), ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

This theorem states that if you have a continuously differentiable function `f` from `E` to `F` over a ring `𝕂` (which could be the real or complex numbers), that has an invertible derivative at a point `a`, then the inverse function of `f` is also continuously differentiable at the point `f(a)`. This inverse function is obtained by applying the `ContDiff.toPartialHomeomorph` function on `f`. The theorem requires the derivative of `f` at `a` to be given by the linear map `f'`, and the differentiability of `f` is specified to a degree `n`, where `n` is a natural number or infinity. Furthermore, `n` should be at least 1. The space `E` is assumed to be complete, which means that every Cauchy sequence in `E` converges to a limit that is also in `E`.

More concisely: If `f: E → F` is a continuously differentiable function with an invertible derivative at `a ∈ E` over a complete ring `𝕂`, then the inverse function `g` of `f` is also continuously differentiable at `b = f(a)` with derivative `g' = (f')⁻¹`.