Yamaguchi Lean 4 Library
ProCGroups.ProC.GroupPredicate
ProCGroups/ProC/GroupPredicate

ProCGroups.ProC.GroupPredicate

1 Structure | 1 Instance

This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.

Open this file on GitHub
import
  • Mathlib.Topology.Algebra.ContinuousMonoidHom
Imported by

Declarations

Structure ProCGroups.ProC.ProCGroupPredicate GitHub 
structure ProCGroupPredicate where
  holds : {G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] → Prop

A predicate packaging the statement that a topological group belongs to a chosen pro-\(C\) class.

Instance ProCGroups.ProC.ProCGroupPredicate.instCoeFunProCGroupPredicate GitHub 
instance instCoeFunProCGroupPredicate : CoeFun ProCGroupPredicate
    (fun _ => {G : Type u} → [Group G] → [TopologicalSpace G] → [IsTopologicalGroup G] → Prop) where
  coe P := @P.holds

A pro-\(C\) group predicate coerces to its underlying predicate.