instNormalCommutatorClosure — Mathlib

English

In a topological group G, the topological closure of the commutator subgroup is a normal subgroup of G.

Русский

В топологической группе G замыкание коммутатора является нормальной подгруппой G.

LaTeX

$$$ (\\mathrm{commutator}(G)).topologicalClosure \\trianglelefteq G$$$

Lean4

instance instNormalCommutatorClosure : (commutator G).topologicalClosure.Normal :=
  Subgroup.is_normal_topologicalClosure (commutator G)

Похожие утверждения