Theorems · Theorem · category theory

CategoryTheory.SmallCategoryOfSet.assoc

∀ {Ω : Type w} (self : CategoryTheory.SmallCategoryOfSet Ω) {X Y Z T : ↑self.obj} (f : ↑(self.hom X Y))
  (g : ↑(self.hom Y Z)) (h : ↑(self.hom Z T)), self.comp (self.comp f g) h = self.comp f (self.comp g h)

Defined in

Mathlib.CategoryTheory.SmallRepresentatives

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms