no goals
ι : Type ?u.23609
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
a : E
r : ℝ
⊢ Convex ℝ (closedBall a r)
simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r