α : Type u_1
ι : Type ?u.23
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)
α : Type u_1
ι : Type ?u.23
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (thickening ε s)
rw [← ball_mul_one]
no goals
α : Type u_1
ι : Type ?u.23
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (ball 1 ε * s)
exact hs.mul_left