case inl
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
⊢ Surjective f

case inr
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ Surjective f
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ Surjective f
cases' hc with hE hc
case inl
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f
case inl
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
⊢ Surjective f
haveI : Subsingleton F := (Equiv.subsingleton_congr f'.toEquiv).1 hE
no goals
case inl
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hE : Subsingleton E
this : Subsingleton F
⊢ Surjective f
exact surjective_to_subsingleton _
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
case inr
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ Surjective f
apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 0) _
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
let p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ Set.range f
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) := by
  have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
  refine' hr.mono fun r hr => Subset.trans _ (image_subset_range f (closedBall 0 r))
  refine' hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr _
  exact subset_univ _
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
⊢ ∀ (x : ℝ), p x → ∀ (y : F), y ∈ closedBall (f 0) x → (fun y => ∃ a, f a = y) y
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ (y : F), y ∈ closedBall (f 0) R → (fun y => ∃ a, f a = y) y
refine' ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono _
no goals
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
⊢ ∀ (x : ℝ), p x → ∀ (y : F), y ∈ closedBall (f 0) x → (fun y => ∃ a, f a = y) y
exact fun R h y hy => h hy
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ↑c < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
rw [sub_pos]
no goals
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ↑c < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
exact hc
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
⊢ ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
⊢ ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r) ⊆ f '' closedBall 0 r
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
⊢ ∀ᶠ (r : ℝ) in atTop, p ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r)
refine' hr.mono fun r hr => Subset.trans _ (image_subset_range f (closedBall 0 r))
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall 0 r ⊆ univ
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) ((↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c) * r) ⊆ f '' closedBall 0 r
refine' hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr _
no goals
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
G : Type ?u.379684
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
G' : Type ?u.379787
inst✝³ : NormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
ε : ℝ
inst✝¹ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
inst✝ : CompleteSpace E
hf : ApproximatesLinearOn f (↑f') univ c
hc : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
hc' : 0 < ↑‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - ↑c
p : ℝ → Prop := fun R => closedBall (f 0) R ⊆ range f
hr✝ : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall 0 r ⊆ univ
exact subset_univ _