# Non-linear maps close to affine maps #

In this file 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 map and `c` is suitably small. Maps of this type behave like `f a + f' (x - a)` near each `a ∈ s`.

When `f'` is onto, we show that `f` is locally onto.

When `f'` is a continuous linear equiv, we show that `f` is a homeomorphism between `s` and `f '' s`. More precisely, we define `ApproximatesLinearOn.toOpenPartialHomeomorph` to be an `OpenPartialHomeomorph` with `toFun = f`, `source = s`, and `target = f '' s`. between `s` and `f '' s`. More precisely, we define `ApproximatesLinearOn.toOpenPartialHomeomorph` to be an `OpenPartialHomeomorph` with `toFun = 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 `ApproximatesLinearOn.toOpenPartialHomeomorph` will imply that the locally inverse function and `ApproximatesLinearOn.toOpenPartialHomeomorph` 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

- to prove a lower estimate on the size of the domain of the inverse function;

- to reuse parts of the proofs in the case if a function is not strictly differentiable. E.g., for a function `f : E × F → G` with estimates on `f x y₁ - f x y₂` but not on `f x₁ y - f x₂ y`.

## Notation #

We introduce some `local notation` to make formulas shorter:

- by `N` we denote `‖f'⁻¹‖`;
- by `g` we denote the auxiliary contracting map `x ↦ x + f'.symm (y - f x)` used to prove that `{x | f x = y}` is nonempty.

source
def ApproximatesLinearOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) (s : Set E) (c : NNReal) :
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

- ApproximatesLinearOn f f' s c = ∀ x ∈ s, ∀ y ∈ s, ‖f x - f y - f' (x - y)‖ ≤ ↑c * ‖x - y‖

Instances For

source
@[simp]
theorem approximatesLinearOn_empty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (f' : E →L[𝕜] F) (c : NNReal) :
ApproximatesLinearOn f f' ∅ c

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

source
theorem ApproximatesLinearOn.mono_num {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c c' : NNReal} (hc : c ≤ c') (hf : ApproximatesLinearOn f f' s c) :
ApproximatesLinearOn f f' s c'
source
theorem ApproximatesLinearOn.mono_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s t : Set E} {c : NNReal} (hst : s ⊆ t) (hf : ApproximatesLinearOn f f' t c) :
ApproximatesLinearOn f f' s c
source
theorem ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s
source
theorem LipschitzOnWith.approximatesLinearOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
LipschitzOnWith c (f - ⇑f') s → ApproximatesLinearOn f f' s c

Alias of the reverse direction of `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`.

source
theorem ApproximatesLinearOn.lipschitzOnWith {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} :
ApproximatesLinearOn f f' s c → LipschitzOnWith c (f - ⇑f') s

Alias of the forward direction of `ApproximatesLinearOn.approximatesLinearOn_iff_lipschitzOnWith`.

source
theorem ApproximatesLinearOn.lipschitz_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
LipschitzWith c fun (x : ↑s) => f ↑x - f' ↑x
source
theorem ApproximatesLinearOn.lipschitz {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
LipschitzWith (‖f'‖₊ + c) (s.restrict f)
source
theorem ApproximatesLinearOn.continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
Continuous (s.restrict f)
source
theorem ApproximatesLinearOn.continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f f' s c) :
ContinuousOn f s

We prove that a function which is linearly approximated by a continuous linear map with a nonlinear right inverse is locally onto. This will apply to the case where the approximating map is a linear equivalence, for the local inverse theorem, but also whenever the approximating map is onto, by Banach's open mapping theorem.

source
theorem ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {ε : ℝ} {b : E} (ε0 : 0 ≤ ε) (hε : Metric.closedBall b ε ⊆ s) :
Set.SurjOn f (Metric.closedBall b ε) (Metric.closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε))

If a function is linearly approximated by a continuous linear map with a (possibly nonlinear) right inverse, then it is locally onto: a ball of an explicit radius is included in the image of the map.

source
theorem ApproximatesLinearOn.open_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) (hs : IsOpen s) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) :
IsOpen (f '' s)
source
theorem ApproximatesLinearOn.image_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s ∈ nhds x) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) :
f '' s ∈ nhds (f x)
source
theorem ApproximatesLinearOn.map_nhds_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} [CompleteSpace E] {s : Set E} {c : NNReal} {f' : E →L[𝕜] F} (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E} (hs : s ∈ nhds x) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) :
Filter.map f (nhds x) = nhds (f x)

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'⁻¹‖`.

source
theorem ApproximatesLinearOn.antilipschitz {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)
source
theorem ApproximatesLinearOn.injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
Function.Injective (s.restrict f)
source
theorem ApproximatesLinearOn.injOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
Set.InjOn f s
source
theorem ApproximatesLinearOn.surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') Set.univ c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
Function.Surjective f
source
def ApproximatesLinearOn.toPartialEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
PartialEquiv E F

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

This is a first step towards the inverse function.

Equations

- hf.toPartialEquiv hc = Set.InjOn.toPartialEquiv f s ⋯

Instances For

source
theorem ApproximatesLinearOn.inverse_continuousOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
ContinuousOn (↑(hf.toPartialEquiv hc).symm) (f '' s)

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

source
theorem ApproximatesLinearOn.to_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
ApproximatesLinearOn (↑(hf.toPartialEquiv hc).symm) (↑f'.symm) (f '' s) (‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c)

The inverse function is approximated linearly on `f '' s` by `f'.symm`.

source
def ApproximatesLinearOn.toOpenPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
OpenPartialHomeomorph E F

Given a function `f` that approximates a linear equivalence on an open set `s`, returns a open partial homeomorphism with `toFun = f` and `source = s`.

Equations

- ApproximatesLinearOn.toOpenPartialHomeomorph f s hf hc hs = { toPartialEquiv := hf.toPartialEquiv hc, open_source := hs, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

Instances For

source
@[deprecated ApproximatesLinearOn.toOpenPartialHomeomorph (since := "2025-08-29")]
def ApproximatesLinearOn.toPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
OpenPartialHomeomorph E F

Alias of `ApproximatesLinearOn.toOpenPartialHomeomorph`.

Given a function `f` that approximates a linear equivalence on an open set `s`, returns a open partial homeomorphism with `toFun = f` and `source = s`.

Equations

- @ApproximatesLinearOn.toPartialHomeomorph = @ApproximatesLinearOn.toOpenPartialHomeomorph

Instances For

source
@[simp]
theorem ApproximatesLinearOn.toOpenPartialHomeomorph_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
↑(toOpenPartialHomeomorph f s hf hc hs) = f
source
@[deprecated ApproximatesLinearOn.toOpenPartialHomeomorph_coe (since := "2025-08-29")]
theorem ApproximatesLinearOn.toPartialHomeomorph_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
↑(toOpenPartialHomeomorph f s hf hc hs) = f

Alias of `ApproximatesLinearOn.toOpenPartialHomeomorph_coe`.

source
@[simp]
theorem ApproximatesLinearOn.toOpenPartialHomeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
(toOpenPartialHomeomorph f s hf hc hs).source = s
source
@[deprecated ApproximatesLinearOn.toOpenPartialHomeomorph_source (since := "2025-08-29")]
theorem ApproximatesLinearOn.toPartialHomeomorph_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
(toOpenPartialHomeomorph f s hf hc hs).source = s

Alias of `ApproximatesLinearOn.toOpenPartialHomeomorph_source`.

source
@[simp]
theorem ApproximatesLinearOn.toOpenPartialHomeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
(toOpenPartialHomeomorph f s hf hc hs).target = f '' s
source
@[deprecated ApproximatesLinearOn.toOpenPartialHomeomorph_target (since := "2025-08-29")]
theorem ApproximatesLinearOn.toPartialHomeomorph_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} (s : Set E) {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) :
(toOpenPartialHomeomorph f s hf hc hs).target = f '' s

Alias of `ApproximatesLinearOn.toOpenPartialHomeomorph_target`.

source
def ApproximatesLinearOn.toHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) {f' : E ≃L[𝕜] F} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') Set.univ c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) :
E ≃ₜ F

A function `f` that approximates a linear equivalence on the whole space is a homeomorphism.

Equations

- ApproximatesLinearOn.toHomeomorph f hf hc = (ApproximatesLinearOn.toOpenPartialHomeomorph f Set.univ hf hc ⋯).toHomeomorphOfSourceEqUnivTargetEqUniv ⋯ ⋯

Instances For

source
theorem ApproximatesLinearOn.closedBall_subset_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ε : ℝ} {f : E → F} {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal} [CompleteSpace E] (hf : ApproximatesLinearOn f (↑f') s c) (hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹) (hs : IsOpen s) {b : E} (ε0 : 0 ≤ ε) (hε : Metric.closedBall b ε ⊆ s) :
Metric.closedBall (f b) ((↑‖↑f'.symm‖₊⁻¹ - ↑c) * ε) ⊆ (toOpenPartialHomeomorph f s hf hc hs).target