α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk '' s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
⊢ IsOpenMap mk
intro s s_op
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk '' s)
change IsOpen (((↑) : G → G ⧸ N) ⁻¹' ((↑) '' s))
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => y * ↑x) ⁻¹' s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (mk ⁻¹' (mk '' s))
rw [QuotientGroup.preimage_image_mk N s]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
N : Subgroup G
n : Subgroup.Normal N
s : Set G
s_op : IsOpen s
⊢ IsOpen (⋃ (x : { x // x ∈ N }), (fun y => y * ↑x) ⁻¹' s)
exact isOpen_iUnion fun n => (continuous_mul_right _).isOpen_preimage s s_op