α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), (fun x => x / a) '' s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
hs : IsOpen s
⊢ IsOpen (s / t)
rw [← iUnion_div_right_image]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : TopologicalGroup α
s t : Set α
hs : IsOpen s
⊢ IsOpen (⋃ (a : α) (_ : a ∈ t), (fun x => x / a) '' s)
exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs