# Documentation

Mathlib.Analysis.Calculus.Deriv.Inverse

# Inverse function theorem - the easy half #

In this file we prove that g' (f x) = (f' x)⁻¹ provided that f is strictly differentiable at x, f' x ≠ 0, and g is a local left inverse of f that is continuous at f x. This is the easy half of the inverse function theorem: the harder half states that g exists.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of Analysis/Calculus/Deriv/Basic.

## Keywords #

derivative, inverse function

theorem HasStrictDerivAt.hasStrictFDerivAt_equiv {𝕜 : Type u} {f : 𝕜𝕜} {f' : 𝕜} {x : 𝕜} (hf : HasStrictDerivAt f f' x) (hf' : f' 0) :
HasStrictFDerivAt f (↑(↑() (Units.mk0 f' hf'))) x
theorem HasDerivAt.hasFDerivAt_equiv {𝕜 : Type u} {f : 𝕜𝕜} {f' : 𝕜} {x : 𝕜} (hf : HasDerivAt f f' x) (hf' : f' 0) :
HasFDerivAt f (↑(↑() (Units.mk0 f' hf'))) x
theorem HasStrictDerivAt.of_local_left_inverse {𝕜 : Type u} {f : 𝕜𝕜} {g : 𝕜𝕜} {f' : 𝕜} {a : 𝕜} (hg : ) (hf : HasStrictDerivAt f f' (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem LocalHomeomorph.hasStrictDerivAt_symm {𝕜 : Type u} (f : ) {a : 𝕜} {f' : 𝕜} (ha : a f.target) (hf' : f' 0) (htff' : HasStrictDerivAt (f) f' (↑() a)) :

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a in the strict sense, then f.symm has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasDerivAt.of_local_left_inverse {𝕜 : Type u} {f : 𝕜𝕜} {g : 𝕜𝕜} {f' : 𝕜} {a : 𝕜} (hg : ) (hf : HasDerivAt f f' (g a)) (hf' : f' 0) (hfg : ∀ᶠ (y : 𝕜) in nhds a, f (g y) = y) :

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a, then g has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem LocalHomeomorph.hasDerivAt_symm {𝕜 : Type u} (f : ) {a : 𝕜} {f' : 𝕜} (ha : a f.target) (hf' : f' 0) (htff' : HasDerivAt (f) f' (↑() a)) :
HasDerivAt (↑()) f'⁻¹ a

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has a nonzero derivative f' at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasDerivAt.eventually_ne {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) (hf' : f' 0) :
∀ᶠ (z : 𝕜) in nhdsWithin x {x}, f z f x
theorem HasDerivAt.tendsto_punctured_nhds {𝕜 : Type u} {F : Type v} [] {f : 𝕜F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) (hf' : f' 0) :
theorem not_differentiableWithinAt_of_local_left_inverse_hasDerivWithinAt_zero {𝕜 : Type u} {f : 𝕜𝕜} {g : 𝕜𝕜} {a : 𝕜} {s : Set 𝕜} {t : Set 𝕜} (ha : a s) (hsu : ) (hf : HasDerivWithinAt f 0 t (g a)) (hst : Set.MapsTo g s t) (hfg : f g =ᶠ[] id) :
theorem not_differentiableAt_of_local_left_inverse_hasDerivAt_zero {𝕜 : Type u} {f : 𝕜𝕜} {g : 𝕜𝕜} {a : 𝕜} (hf : HasDerivAt f 0 (g a)) (hfg : f g =ᶠ[nhds a] id) :