E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.166456
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C✝ : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
C : ℝ≥0
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.166456
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C✝ : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
C : ℝ≥0
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s
rw [lipschitzOnWith_iff_norm_sub_le]
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.166456
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C✝ : ℝ
s : Set E
x✝ y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
C : ℝ≥0
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑C * ‖x - y‖
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.166456
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C✝ : ℝ
s : Set E
x y : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
C : ℝ≥0
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖
intro x x_in y y_in
no goals
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.166456
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C✝ : ℝ
s : Set E
x✝ y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
C : ℝ≥0
hf : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
bound : ∀ (x : E), x ∈ s → ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑C * ‖x - y‖
exact hs.norm_image_sub_le_of_norm_hasFDerivWithin_le hf bound y_in x_in