Theorems · Theorem · category theory
SimplexCategory.const_comp
∀ (x : SimplexCategory) {y z : SimplexCategory} (f : y ⟶ z) (i : Fin (y.len + 1)),
CategoryTheory.CategoryStruct.comp (x.const y i) f = x.const z ((SimplexCategory.Hom.toOrderHom f) i)- Cited by
- 7 results in Mathlib
- Foundations
- Depth 31 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- SimplexCategorystatement and proof · cited by 2,204
- OrderHomstatement · cited by 934
- SimplexCategory.lenstatement and proof · cited by 542
- SimplexCategory.Hom.toOrderHomstatement · cited by 111
- SimplexCategory.conststatement · cited by 47
Cited by7
Results whose statement or proof uses this declaration.
- SSet.Truncated.spine_map_vertexproof · cited by 1
- SimplexCategory.const_subinterval_eqproof · cited by 1
- SSet.StrictSegal.spine_δ_vertex_geproof · cited by 0
- SSet.StrictSegal.spine_δ_vertex_ltproof · cited by 0
- SimplexCategory.const_fac_thru_zeroproof · cited by 0
- SSet.Truncated.StrictSegal.spine_δ_vertex_geproof · cited by 0
- SSet.Truncated.StrictSegal.spine_δ_vertex_ltproof · cited by 0