α : 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 : α
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
inst✝ : Normal N
n : G
hn : n ∈ topologicalClosure N
g : G
⊢ MapsTo (fun h => g * h * g⁻¹) ↑N ↑N
α : 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 : α
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
inst✝ : Normal N
n : G
hn : n ∈ topologicalClosure N
g : G
⊢ g * n * g⁻¹ ∈ topologicalClosure N
apply map_mem_closure (TopologicalGroup.continuous_conj g) hn
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 : α
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
N : Subgroup G
inst✝ : Normal N
n : G
hn : n ∈ topologicalClosure N
g : G
⊢ MapsTo (fun h => g * h * g⁻¹) ↑N ↑N
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g