α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
ht : IsOpen t
⊢ IsOpen (⋃ (a : α) (_ : a ∈ s), a • t)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
ht : IsOpen t
⊢ IsOpen (s • t)
rw [← iUnion_smul_set]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : ContinuousConstSMul α β
s : Set α
t : Set β
ht : IsOpen t
⊢ IsOpen (⋃ (a : α) (_ : a ∈ s), a • t)
exact isOpen_biUnion fun a _ => ht.smul _