Module

BasisAtOne.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.BasisAtOne

1 declaration indexed from sourceView source ↗

Module documentation

Open-normal neighborhood bases at the identity

Every identity neighborhood in a profinite group contains an open normal subgroup. This file packages that refinement result for later basis, separation, and inverse-limit arguments.

Imports1

Mathlib.Topology.Algebra.ClopenNhdofOne

Imported by12

theorem

exists_openNormalSubgroup_sub_open_nhds_of_one

L28 ↗

ProCGroups.ProC.exists_openNormalSubgroup_sub_open_nhds_of_one

Documentation

In a compact totally disconnected topological group, any open neighborhood of \(1\) contains an open normal subgroup.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem exists_openNormalSubgroup_sub_open_nhds_of_one [CompactSpace G]
    [TotallyDisconnectedSpace G] {W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
    ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) : Set G) ⊆ W

Module documentation

Open-normal neighborhood bases at the identity

Declarations

exists_openNormalSubgroup_sub_open_nhds_of_one