α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ (a : α) (_ : a ∈ s), a • t)
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (s * t)
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
ht : IsUpperSet t
⊢ IsUpperSet (⋃ (a : α) (_ : a ∈ s), a • t)
exact isUpperSet_iUnion₂ fun x _ ↦ ht.smul