NYLL
Module

SubgroupCommutator.lean

Nyll.ProCGroups.Abelian.SubgroupCommutator
1 declaration indexed from sourceView source ↗

Module documentation

Closed commutators of closed subgroups

For a closed subgroup, the image of its closed commutator under the subgroup inclusion is the topological closure of its commutator in the ambient group.

Imports1
Imported by2

Declarations

theorem

map_closedCommutator_subtype

L22 ↗
ProCGroups.Abelian.map_closedCommutator_subtype
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped commutatorElement
namespace ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients ProCGroups.Abelian
universe u
Lean source · statement
theorem map_closedCommutator_subtype
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (D : Subgroup G) (hD : IsClosed (D : Set G)) :
    (Subgroup.closedCommutator D).map D.subtype = ⁅D, D⁆.topologicalClosure

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.