Theorems · Definition · Lie groups

ProfiniteGrp.of

(G : Type u) →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] → [CompactSpace G] → [TotallyDisconnectedSpace G] → ProfiniteGrp.{u}

Construct a term of ProfiniteGrp from a type endowed with the structure of a compact and totally disconnected topological group. (The condition of being Hausdorff can be omitted here because totally disconnected implies that {1} is a closed set, thus implying Hausdorff in a topological group.)

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

8 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroupCompactSpaceTotallyDisconnectedSpace