M : Type ?u.142323
α : Type ?u.142326
β : Type ?u.142329
Γ : Type u_1
inst✝³ : Group Γ
T : Type u_2
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (⋃ (a : Γ), (fun x x_1 => x • x_1) a '' U)
M : Type ?u.142323
α : Type ?u.142326
β : Type ?u.142329
Γ : Type u_1
inst✝³ : Group Γ
T : Type u_2
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (Quotient.mk' '' U)
rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
no goals
M : Type ?u.142323
α : Type ?u.142326
β : Type ?u.142329
Γ : Type u_1
inst✝³ : Group Γ
T : Type u_2
inst✝² : TopologicalSpace T
inst✝¹ : MulAction Γ T
inst✝ : ContinuousConstSMul Γ T
U : Set T
hU : IsOpen U
⊢ IsOpen (⋃ (a : Γ), (fun x x_1 => x • x_1) a '' U)
exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU