Theorems · Theorem · real analysis

OpenPartialHomeomorph.contDiffAt_symm

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  [CompleteSpace E] (f : OpenPartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F},
  a ∈ f.target → HasFDerivAt (↑f) (↑f₀') (↑f.symm a) → ContDiffAt 𝕜 n (↑f) (↑f.symm a) → ContDiffAt 𝕜 n (↑f.symm) a

If f is a local homeomorphism and the point a is in its target, and if f is n times continuously differentiable at f.symm a, and if the derivative at f.symm a is a continuous linear equivalence, 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.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Operations

Cited by

3 results in Mathlib

Foundations

Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpace