Theorems · Definition · algebraic topology
SSet.Truncated.Edge.id
{X : SSet.Truncated 2} →
(x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })) → SSet.Truncated.Edge x xThe constant edge on a 0-simplex.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functor.mapproof · cited by 8,698
- Oppositestatement · cited by 8,081
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- SimplexCategorystatement · cited by 2,204
- Quiver.Hom.opproof · cited by 1,948
- SimplexCategory.lenstatement · cited by 542
- SimplexCategory.Truncatedstatement · cited by 236
- SSet.Truncatedstatement and proof · cited by 214
- SSet.Truncated.Edgestatement · cited by 81
- SimplexCategory.Truncated.σ₂proof · cited by 20
Cited by28
Results whose statement or proof uses this declaration.
- SSet.Edge.idproof · cited by 24
- SSet.Truncated.Edge.CompStruct.idCompstatement · cited by 10
- SSet.Truncated.HomotopicLproof · cited by 8
- SSet.Truncated.Edge.CompStruct.compIdstatement · cited by 7
- SSet.Truncated.HomotopicRproof · cited by 7
- SSet.Truncated.HomotopyCategory.liftstatement and proof · cited by 2
- SSet.Truncated.HomotopicL.homotopicRproof · cited by 2
- SSet.Truncated.HomotopicR.homotopicLproof · cited by 2
- SSet.Truncated.Edge.CompStruct.comp_uniqueproof · cited by 1
- SSet.Truncated.Edge.CompStruct.idCompIdstatement and proof · cited by 1
- SSet.Truncated.Edge.CompStruct.idCompId_simplexstatement · cited by 1
- SSet.Truncated.Edge.id_edgestatement and proof · cited by 1