case inl
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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
hE : Subsingleton E
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)

case inr
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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 : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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')‖₊⁻¹
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
cases' hc with hE hc
case h.e'_6.h
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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 : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x✝ : ↑s
⊢ restrict s f x✝ = restrict s (↑f') x✝ + (f ↑x✝ - ↑↑f' ↑x✝)
case inr
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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 : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
convert(f'.antilipschitz.restrict s).add_lipschitzWith hf.lipschitz_sub hc
no goals
case h.e'_6.h
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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 : c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
x✝ : ↑s
⊢ restrict s f x✝ = restrict s (↑f') x✝ + (f ↑x✝ - ↑↑f' ↑x✝)
simp [restrict]
case inl
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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
hE : Subsingleton E
this : Subsingleton ↑s
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
case inl
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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
hE : Subsingleton E
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
haveI : Subsingleton s := ⟨fun x y => Subtype.eq <| @Subsingleton.elim _ hE _ _⟩
no goals
case inl
𝕜 : 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.329645
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.329748
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
hE : Subsingleton E
this : Subsingleton ↑s
⊢ AntilipschitzWith (‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹ - c)⁻¹ (restrict s f)
exact AntilipschitzWith.of_subsingleton