α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : ↑(Subgroup.topologicalClosure s) = ↑⊤
⊢ ↑(Subgroup.topologicalClosure (Subgroup.map f s)) = ↑⊤
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs : Subgroup.topologicalClosure s = ⊤
⊢ Subgroup.topologicalClosure (Subgroup.map f s) = ⊤
rw [SetLike.ext'_iff] at hs⊢
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : ↑(Subgroup.topologicalClosure s) = ↑⊤
⊢ ↑(Subgroup.topologicalClosure (Subgroup.map f s)) = ↑⊤
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs⊢
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁶ : TopologicalSpace G
inst✝⁵ : Group G
inst✝⁴ : TopologicalGroup G
inst✝³ : TopologicalSpace α
f✝ : α → G
s✝ : Set α
x : α
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
hf' : DenseRange ↑f
s : Subgroup G
hs✝ : Subgroup.topologicalClosure s = ⊤
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)
exact hf'.dense_image hf hs