α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), MulOpposite.op a • s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (s * t)
rw [← iUnion_op_smul_set]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), MulOpposite.op a • s)
exact isOpen_biUnion fun a _ => hs.smul _