α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)
rw [div_eq_mul_inv]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)
exact ht.inv.mul_left