no goals
E : Type ?u.273429
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.273525
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_1
G : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
x✝ y : 𝕜
C : ℝ≥0
hs : Convex ℝ s
hf : ∀ (x : 𝕜), x ∈ s → HasDerivWithinAt f (f' x) s x
bound : ∀ (x : 𝕜), x ∈ s → ‖f' x‖₊ ≤ C
x : 𝕜
hx : x ∈ s
⊢ ‖smulRight 1 (f' x)‖₊ ≤ ‖f' x‖₊
simp