α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ (⋃ (a : α) (_ : a ∈ Set.Ici 1), a • ↑s) ⊆ ↑s
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ Set.Ici 1 * ↑s ⊆ ↑s
rw [← smul_eq_mul, ← Set.iUnion_smul_set]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s✝ t : Set α
a : α
s : UpperSet α
⊢ (⋃ (a : α) (_ : a ∈ Set.Ici 1), a • ↑s) ⊆ ↑s
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset