Theorems · Theorem · real analysis

OpenPartialHomeomorph.hasStrictDerivAt_symm

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (f : OpenPartialHomeomorph 𝕜 𝕜) {a f' : 𝕜},
  a ∈ f.target → f' ≠ 0 → HasStrictDerivAt (↑f) f' (↑f.symm a) → HasStrictDerivAt (↑f.symm) f'⁻¹ a

If f is an open partial homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a in the strict sense, then f.symm 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.Deriv.Inverse

Cited by

6 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedField