Theorems · Theorem · several complex variables

AnalyticAt.analyticAt_localInverse

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [inst_1 : CompleteSpace 𝕜] [CharZero 𝕜]
  (hf : AnalyticAt 𝕜 f x) (hf' : deriv f x ≠ 0),
  AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

The local inverse of an analytic function (at a point where its derivative does not vanish) is itself analytic.

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpaceCharZero