ι : Type ?u.26868
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)
ι : Type ?u.26868
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (Metric.thickening δ s)
rw [← add_ball_zero]
no goals
ι : Type ?u.26868
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Set E
hs : Convex ℝ s
δ : ℝ
⊢ Convex ℝ (s + ball 0 δ)
exact hs.add (convex_ball 0 _)