α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)
rw [mul_comm]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)
exact hs.mul_left