theorem
L23 ↗isAbFaithful
ProCGroups.FiniteStepSolvableQuotients.IsSigmaAbFaithful.isAbFaithful
The stronger Sigma condition implies the ordinary condition on all open subgroups and all their open normal subgroups.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.FiniteStepSolvableQuotients
universe uLean source · statement
theorem IsSigmaAbFaithful.isAbFaithful {sigma : Set ℕ} {G : Type u}
[Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hG : IsSigmaAbFaithful sigma G) : IsAbFaithful G