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