Theorems · Theorem · real analysis

HasStrictFDerivAt.of_local_left_inverse

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F}
  {g : F → E} {a : F},
  ContinuousAt g a →
    HasStrictFDerivAt f (↑f') (g a) → (∀ᶠ (y : F) in nhds a, f (g y) = y) → HasStrictFDerivAt g (↑f'.symm) a

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense. 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.FDeriv.OfCompLeft

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace