ProCGroups.FiniteGeneration.topologicallyFinitelyGenerated_openSubgroup
An open subgroup of a finitely generated profinite group has an actual finite topological generating set.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.FiniteGeneration
open ProCGroups.Generation
universe uLean source · statement
theorem topologicallyFinitelyGenerated_openSubgroup
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
(hfg : TopologicallyFinitelyGenerated G) (U : OpenSubgroup G) :
TopologicallyFinitelyGenerated (U : Subgroup G)