mathlib documentation

analysis.calculus.inverse

Inverse function theorem

In this file we prove the inverse function theorem. It says that if a map f : E → F has an invertible strict derivative f' at a, then it is locally invertible, and the inverse function has derivative f' ⁻¹.

We define has_strict_deriv_at.to_local_homeomorph that repacks a function f with a hf : has_strict_fderiv_at f f' a, f' : E ≃L[𝕜] F, into a local_homeomorph. The to_fun of this local_homeomorph is defeq to f, so one can apply theorems about local_homeomorph to hf.to_local_homeomorph f, and get statements about f.

Then we define has_strict_fderiv_at.local_inverse to be the inv_fun of this local_homeomorph, and prove two versions of the inverse function theorem:

In the one-dimensional case we reformulate these theorems in terms of has_strict_deriv_at and f'⁻¹.

We also reformulate the theorems in terms of times_cont_diff, to give that C^k (respectively, smooth) inputs give C^k (smooth) inverses. These versions require that continuous differentiability implies strict differentiability; this is false over a general field, true over (the setting in which it is implemented here), and true but (TODO) not yet implemented over .

Some related theorems, providing the derivative and higher regularity assuming that we already know the inverse function, are formulated in fderiv.lean, deriv.lean, and times_cont_diff.lean.

Notations

In the section about approximates_linear_on we introduce some local notation to make formulas shorter:

Tags

derivative, strictly differentiable, continuously differentiable, smooth, inverse function

Non-linear maps approximating close to affine maps

In this section we study a map f such that ∥f x - f y - f' (x - y)∥ ≤ c * ∥x - y∥ on an open set s, where f' : E ≃L[𝕜] F is a continuous linear equivalence and c < ∥f'⁻¹∥. Maps of this type behave like f a + f' (x - a) near each a ∈ s.

If E is a complete space, we prove that the image f '' s is open, and f is a homeomorphism between s and f '' s. More precisely, we define approximates_linear_on.to_local_homeomorph to be a local_homeomorph with to_fun = f, source = s, and target = f '' s.

Maps of this type naturally appear in the proof of the inverse function theorem (see next section), and approximates_linear_on.to_local_homeomorph will imply that the locally inverse function exists.

We define this auxiliary notion to split the proof of the inverse function theorem into small lemmas. This approach makes it possible

def approximates_linear_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
(E → F)(E →L[𝕜] F)set Eℝ≥0 → Prop

We say that f approximates a continuous linear map f' on s with constant c, if ∥f x - f y - f' (x - y)∥ ≤ c * ∥x - y∥ whenever x, y ∈ s.

This predicate is defined to facilitate the splitting of the inverse function theorem into small lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined on a specific set.

Equations

First we prove some properties of a function that approximates_linear_on a (not necessarily invertible) continuous linear map.

theorem approximates_linear_on.mono_num {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c c' : ℝ≥0} :
c c'approximates_linear_on f f' s capproximates_linear_on f f' s c'

theorem approximates_linear_on.mono_set {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s t : set E} {c : ℝ≥0} :
s tapproximates_linear_on f f' t capproximates_linear_on f f' s c

theorem approximates_linear_on.lipschitz_sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : ℝ≥0} :
approximates_linear_on f f' s clipschitz_with c (λ (x : s), f x - f' x)

theorem approximates_linear_on.lipschitz {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : ℝ≥0} :

theorem approximates_linear_on.continuous {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : ℝ≥0} :

theorem approximates_linear_on.continuous_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : set E} {c : ℝ≥0} :

From now on we assume that f approximates an invertible continuous linear map f : E ≃L[𝕜] F.

We also assume that either E = {0}, or c < ∥f'⁻¹∥⁻¹. We use N as an abbreviation for ∥f'⁻¹∥.

theorem approximates_linear_on.antilipschitz {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} :

theorem approximates_linear_on.injective {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} :

theorem approximates_linear_on.inj_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} :

def approximates_linear_on.to_local_equiv {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} :

A map approximating a linear equivalence on a set defines a local equivalence on this set. Should not be used outside of this file, because it is superseded by to_local_homeomorph below.

This is a first step towards the inverse function.

Equations
theorem approximates_linear_on.inverse_continuous_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) :

The inverse function is continuous on f '' s. Use properties of local_homeomorph instead.

Now we prove that f '' s is an open set. This follows from the fact that the restriction of f on s is an open map. More precisely, we show that the image of a closed ball $$\bar B(a, ε) ⊆ s$$ under f includes the closed ball $$\bar B\left(f(a), frac{ε}{∥{f'}⁻¹∥⁻¹-c}\right)$$.

In order to do this, we introduce an auxiliary map $$g_y(x) = x + {f'}⁻¹ (y - f x)$$. Provided that $$∥y - f a∥ ≤ frac{ε}{∥{f'}⁻¹∥⁻¹-c}$$, we prove that $$g_y$$ contracts in $$\bar B(a, ε)$$ and f sends the fixed point of $$g_y$$ to y.

def approximates_linear_on.inverse_approx_map {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] :
(E → F)(E ≃L[𝕜] F)F → E → E

Iterations of this map converge to f⁻¹ y. The formula is very similar to the one used in Newton's method, but we use the same f'.symm for all y instead of evaluating the derivative at each point along the orbit.

Equations
theorem approximates_linear_on.inverse_approx_map_sub {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} (y : F) (x x' : E) :

theorem approximates_linear_on.inverse_approx_map_dist_self {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} (y : F) (x : E) :

theorem approximates_linear_on.inverse_approx_map_dist_self_le {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} (y : F) (x : E) :

theorem approximates_linear_on.inverse_approx_map_fixed_iff {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} (y : F) {x : E} :

theorem approximates_linear_on.inverse_approx_map_contracts_on {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} (y : F) (hf : approximates_linear_on f f' s c) {x x' : E} :

theorem approximates_linear_on.inverse_approx_map_maps_to {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} {y : F} {ε : } (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) {b : E} :

theorem approximates_linear_on.surj_on_closed_ball {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} {ε : } (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) {b : E} :

def approximates_linear_on.to_local_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) {f' : E ≃L[𝕜] F} (s : set E) {c : ℝ≥0} :

Given a function f that approximates a linear equivalence on an open set s, returns a local homeomorph with to_fun = f and source = s.

Equations
@[simp]
theorem approximates_linear_on.to_local_homeomorph_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) (hs : is_open s) :

@[simp]
theorem approximates_linear_on.to_local_homeomorph_source {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) (hs : is_open s) :

@[simp]
theorem approximates_linear_on.to_local_homeomorph_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) (hs : is_open s) :

theorem approximates_linear_on.closed_ball_subset_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {s : set E} {c : ℝ≥0} {ε : } (hf : approximates_linear_on f f' s c) (hc : subsingleton E c < (nnnorm (f'.symm))⁻¹) (hs : is_open s) {b : E} :

Inverse function theorem

Now we prove the inverse function theorem. Let f : E → F be a map defined on a complete vector space E. Assume that f has an invertible derivative f' : E ≃L[𝕜] F at a : E in the strict sense. Then f approximates f' in the sense of approximates_linear_on on an open neighborhood of a, and we can apply approximates_linear_on.to_local_homeomorph to construct the inverse function.

theorem has_strict_fderiv_at.approximates_deriv_on_nhds {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {c : ℝ≥0} :
subsingleton E 0 < c(∃ (s : set E) (H : s 𝓝 a), approximates_linear_on f f' s c)

If f has derivative f' at a in the strict sense and c > 0, then f approximates f' with constant c on some neighborhood of a.

theorem has_strict_fderiv_at.approximates_deriv_on_open_nhds {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} :
has_strict_fderiv_at f f' a(∃ (s : set E) (hs : a s is_open s), approximates_linear_on f f' s ((nnnorm (f'.symm))⁻¹ / 2))

def has_strict_fderiv_at.to_local_homeomorph {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) {f' : E ≃L[𝕜] F} {a : E} :

Given a function with an invertible strict derivative at a, returns a local_homeomorph with to_fun = f and a ∈ source. This is a part of the inverse function theorem. The other part has_strict_fderiv_at.to_local_inverse states that the inverse function of this local_homeomorph has derivative f'.symm.

Equations
@[simp]
theorem has_strict_fderiv_at.to_local_homeomorph_coe {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

theorem has_strict_fderiv_at.mem_to_local_homeomorph_source {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

theorem has_strict_fderiv_at.image_mem_to_local_homeomorph_target {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

def has_strict_fderiv_at.local_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] (f : E → F) (f' : E ≃L[𝕜] F) (a : E) :
has_strict_fderiv_at f f' aF → E

Given a function f with an invertible derivative, returns a function that is locally inverse to f.

Equations
theorem has_strict_fderiv_at.eventually_left_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
∀ᶠ (x : E) in 𝓝 a, has_strict_fderiv_at.local_inverse f f' a hf (f x) = x

theorem has_strict_fderiv_at.local_inverse_apply_image {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

theorem has_strict_fderiv_at.eventually_right_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :
∀ᶠ (y : F) in 𝓝 (f a), f (has_strict_fderiv_at.local_inverse f f' a hf y) = y

theorem has_strict_fderiv_at.local_inverse_continuous_at {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

theorem has_strict_fderiv_at.local_inverse_tendsto {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

theorem has_strict_fderiv_at.local_inverse_unique {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {g : F → E} :
(∀ᶠ (x : E) in 𝓝 a, g (f x) = x)(∀ᶠ (y : F) in 𝓝 (f a), g y = has_strict_fderiv_at.local_inverse f f' a hf y)

theorem has_strict_fderiv_at.to_local_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) :

If f has an invertible derivative f' at a in the sense of strict differentiability (hf), then the inverse function hf.local_inverse f has derivative f'.symm at f a.

theorem has_strict_fderiv_at.to_local_left_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_group F] [normed_space 𝕜 F] [cs : complete_space E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E} (hf : has_strict_fderiv_at f f' a) {g : F → E} :
(∀ᶠ (x : E) in 𝓝 a, g (f x) = x)has_strict_fderiv_at g (f'.symm) (f a)

If f : E → F has an invertible derivative f' at a in the sense of strict differentiability and g (f x) = x in a neighborhood of a, then g has derivative f'.symm at f a.

For a version assuming f (g y) = y and continuity of g at f a but not [complete_space E] see of_local_left_inverse.

Inverse function theorem, 1D case

In this case we prove a version of the inverse function theorem for maps f : 𝕜 → 𝕜. We use continuous_linear_equiv.units_equiv_aut to translate has_strict_deriv_at f f' a and f' ≠ 0 into has_strict_fderiv_at f (_ : 𝕜 ≃L[𝕜] 𝕜) a.

def has_strict_deriv_at.local_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [cs : complete_space 𝕜] (f : 𝕜 → 𝕜) (f' a : 𝕜) :
has_strict_deriv_at f f' af' 0𝕜 → 𝕜

A function that is inverse to f near a.

Equations
theorem has_strict_deriv_at.to_local_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [cs : complete_space 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : has_strict_deriv_at f f' a) (hf' : f' 0) :

theorem has_strict_deriv_at.to_local_left_inverse {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] [cs : complete_space 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜} (hf : has_strict_deriv_at f f' a) (hf' : f' 0) {g : 𝕜 → 𝕜} :
(∀ᶠ (x : 𝕜) in 𝓝 a, g (f x) = x)has_strict_deriv_at g f'⁻¹ (f a)

Inverse function theorem, smooth case

def times_cont_diff_at.to_local_homeomorph {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] (f : E' → F') {f' : E' ≃L[] F'} {a : E'} {n : with_top } :
times_cont_diff_at n f ahas_fderiv_at f f' a1 nlocal_homeomorph E' F'

Given a times_cont_diff function over with an invertible derivative at a, returns a local_homeomorph with to_fun = f and a ∈ source.

Equations
@[simp]
theorem times_cont_diff_at.to_local_homeomorph_coe {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } (hf : times_cont_diff_at n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :

theorem times_cont_diff_at.mem_to_local_homeomorph_source {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } (hf : times_cont_diff_at n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :

theorem times_cont_diff_at.image_mem_to_local_homeomorph_target {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } (hf : times_cont_diff_at n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :

def times_cont_diff_at.local_inverse {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } :
times_cont_diff_at n f ahas_fderiv_at f f' a1 nF' → E'

Given a times_cont_diff function over with an invertible derivative at a, returns a function that is locally inverse to f.

Equations
theorem times_cont_diff_at.local_inverse_apply_image {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } (hf : times_cont_diff_at n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :
hf.local_inverse hf' hn (f a) = a

theorem times_cont_diff_at.to_local_inverse {E' : Type u_6} [normed_group E'] [normed_space E'] {F' : Type u_7} [normed_group F'] [normed_space F'] [complete_space E'] {f : E' → F'} {f' : E' ≃L[] F'} {a : E'} {n : with_top } (hf : times_cont_diff_at n f a) (hf' : has_fderiv_at f f' a) (hn : 1 n) :

Given a times_cont_diff function over with an invertible derivative at a, the inverse function (produced by times_cont_diff.to_local_homeomorph) is also times_cont_diff.