Theorems · Theorem · real analysis

HasStrictDerivAt.eventually_right_inverse

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜}
  (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0),
  ∀ᶠ (x : 𝕜) in nhds (f a), f (HasStrictDerivAt.localInverse f f' a hf hf' x) = x

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpace