Theorems · Theorem · category theory

AugmentedSimplexCategory.inr_comp_inl_comp_associator

∀ (x y z : AugmentedSimplexCategory),
  CategoryTheory.CategoryStruct.comp (x.inr y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z)
        (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) =
    CategoryTheory.CategoryStruct.comp (y.inl z) (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z))

Defined in: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
Cited by: 1 results in Mathlib
Foundations: Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CategoryTheory.Iso.homstatement and proof · cited by 7,684
CategoryTheory.MonoidalCategoryStruct.tensorObjstatement and proof · cited by 3,106
SimplexCategorystatement and proof · cited by 2,204
CategoryTheory.eqToHomproof · cited by 860
CategoryTheory.MonoidalCategoryStruct.associatorstatement and proof · cited by 667
SimplexCategory.lenproof · cited by 542
SimplexCategory.Hom.toOrderHomproof · cited by 111
AugmentedSimplexCategorystatement and proof · cited by 66
OrderHom.extproof · cited by 55

Cited by1

Results whose statement or proof uses this declaration.

AugmentedSimplexCategory.inr_comp_inl_comp_associator_assocproof · cited by 0