Theorems · Definition · Lie groups

ProfiniteAddGrp.limit

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J ProfiniteAddGrp.{max v u} → ProfiniteAddGrp.{max v u}

The abbreviation for the limit of ProfiniteAddGrps.

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory