ProCGroups/ProC/OpenNormalSubgroups/BasisAtOne.lean

1import Mathlib.Topology.Algebra.ClopenNhdofOne

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/BasisAtOne.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Pro-C groups and open normal quotients

14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

15-/

17namespace ProCGroups.ProC

19universe u v

21section

23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

25/-- In a compact totally disconnected topological group,

26any open neighborhood of `1` contains an open normal subgroup. -/

27theorem exists_openNormalSubgroup_sub_open_nhds_of_one [CompactSpace G]

28 [TotallyDisconnectedSpace G] {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :

29 ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) : Set G) ⊆ W := by

30 simpa using ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one hW h1W

32end

34end ProCGroups.ProC