𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.397883
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.397986
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ Continuous (restrict (f '' s) ↑(LocalEquiv.symm (toLocalEquiv hf hc)))
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.397883
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.397986
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ContinuousOn (↑(LocalEquiv.symm (toLocalEquiv hf hc))) (f '' s)
apply continuousOn_iff_continuous_restrict.2
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.397883
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.397986
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ MapsTo (fun x => LocalEquiv.invFun (toLocalEquiv hf hc) x) (toLocalEquiv hf hc).target s
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.397883
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.397986
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ Continuous (restrict (f '' s) ↑(LocalEquiv.symm (toLocalEquiv hf hc)))
refine' ((hf.antilipschitz hc).to_rightInvOn' _ (hf.toLocalEquiv hc).right_inv').continuous
no goals
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.397883
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.397986
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ MapsTo (fun x => LocalEquiv.invFun (toLocalEquiv hf hc) x) (toLocalEquiv hf hc).target s
exact fun x hx => (hf.toLocalEquiv hc).map_target hx