Theorems · Theorem · real analysis

HasStrictDerivAt.to_localInverse

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜}
  (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0),
  HasStrictDerivAt (HasStrictDerivAt.localInverse f f' a hf hf') f'⁻¹ (f a)

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpace