Theorems · Theorem · Lie groups

ProfiniteAddGrp.ofHom_comp

∀ {X Y Z : Type u} [inst : AddGroup X] [inst_1 : TopologicalSpace X] [inst_2 : IsTopologicalAddGroup X]
  [inst_3 : CompactSpace X] [inst_4 : TotallyDisconnectedSpace X] [inst_5 : AddGroup Y] [inst_6 : TopologicalSpace Y]
  [inst_7 : IsTopologicalAddGroup Y] [inst_8 : CompactSpace Y] [inst_9 : TotallyDisconnectedSpace Y]
  [inst_10 : AddGroup Z] [inst_11 : TopologicalSpace Z] [inst_12 : IsTopologicalAddGroup Z] [inst_13 : CompactSpace Z]
  [inst_14 : TotallyDisconnectedSpace Z] (f : X →ₜ+ Y) (g : Y →ₜ+ Z),
  ProfiniteAddGrp.ofHom (g.comp f) =
    CategoryTheory.CategoryStruct.comp (ProfiniteAddGrp.ofHom f) (ProfiniteAddGrp.ofHom g)

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpaceAddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpaceAddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpace