English
Let G be a topological group and N a normal subgroup of G. Then the topological closure of N is a normal subgroup of G.
Русский
Пусть G — топологическая группа и N — нормальная подгруппа G. Тогда топологическое замыкание N является нормальной подгруппой G.
LaTeX
$$$\big(\operatorname{Subgroup.topologicalClosure} N\big) \trianglelefteq G$$$
Lean4
/-- The topological closure of a normal subgroup is normal. -/
@[to_additive /-- The topological closure of a normal additive subgroup is normal. -/
]
theorem is_normal_topologicalClosure {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G)
[N.Normal] : (Subgroup.topologicalClosure N).Normal where
conj_mem n hn
g := by
apply map_mem_closure (IsTopologicalGroup.continuous_conj g) hn
exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g
