Inverse function theorem, 1D case

In this file we prove a version of the inverse function theorem for maps f : 𝕜 → 𝕜. We use ContinuousLinearEquiv.unitsEquivAut to translate HasStrictDerivAt f f' a and f' ≠ 0 into HasStrictFDerivAt f (_ : 𝕜 ≃L[𝕜] 𝕜) a.

@[reducible]

def HasStrictDerivAt.localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] (f : 𝕜 → 𝕜) (f' : 𝕜) (a : 𝕜) (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0) : 𝕜 → 𝕜

A function that is inverse to f near a.

Equations

• One or more equations did not get rendered due to their size.

theorem HasStrictDerivAt.map_nhds_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' : 𝕜} {a : 𝕜} (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0) : Filter.map f (nhds a) = nhds (f a)

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

theorem HasStrictDerivAt.to_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' : 𝕜} {a : 𝕜} (hf : HasStrictDerivAt f f' a) (hf' : f' ≠ 0) {g : 𝕜 → 𝕜} (hg : ∀ᶠ (x : 𝕜) in nhds a, g (f x) = x) : HasStrictDerivAt g f'⁻¹ (f a)

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

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