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, inline]

noncomputable abbrev 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.

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

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

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 (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 isOpenMap_of_hasStrictDerivAt {𝕜 : 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.