Theorems · Theorem · real analysis

isOpenMap_of_hasStrictDerivAt

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f f' : 𝕜 → 𝕜},
  (∀ (x : 𝕜), HasStrictDerivAt f (f' x) x) → (∀ (x : 𝕜), f' x ≠ 0) → IsOpenMap f

If a function has a non-zero strict derivative at all points, then it is an open map.

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldCompleteSpace