𝕜 : 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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
this : ∀ (x y : E), f x - f y - ↑f' (x - y) = (f - ↑f') x - (f - ↑f') y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ↑f') 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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ↑f') s
have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y := fun x y ↦ by
  simp only [map_sub, Pi.sub_apply]; abel
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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
this : ∀ (x y : E), f x - f y - ↑f' (x - y) = (f - ↑f') x - (f - ↑f') y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ↑f') s
simp only [this, lipschitzOnWith_iff_norm_sub_le, ApproximatesLinearOn]
𝕜 : 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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - (↑f' x - ↑f' y) = f x - ↑f' x - (f y - ↑f' y)
𝕜 : 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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - ↑f' (x - y) = (f - ↑f') x - (f - ↑f') y
simp only [map_sub, Pi.sub_apply]
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.26755
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
G' : Type ?u.26858
inst✝² : NormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
ε : ℝ
inst✝ : CompleteSpace E
f✝ : E → F
f'✝ : E →L[𝕜] F
s✝ t : Set E
c✝ c' : ℝ≥0
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - (↑f' x - ↑f' y) = f x - ↑f' x - (f y - ↑f' y)
abel