Theorems · Definition · algebraic topology

SSet.Truncated.Edge.CompStruct.idCompId

{X : SSet.Truncated 2} →
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })) →
    (SSet.Truncated.Edge.id x).CompStruct (SSet.Truncated.Edge.id x) (SSet.Truncated.Edge.id x)

Edge.id x is a composition of Edge.id x with Edge.id x.

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
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.

Cites9

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

CategoryTheory.Functor.objstatement and proof · cited by 19,642
Oppositestatement · cited by 8,081
SimplexCategorystatement · cited by 2,204
SimplexCategory.lenstatement · cited by 542
SimplexCategory.Truncatedstatement · cited by 236
SSet.Truncatedstatement and proof · cited by 214
SSet.Truncated.Edge.CompStructstatement · cited by 28
SSet.Truncated.Edge.idstatement and proof · cited by 20
SSet.Truncated.Edge.CompStruct.idCompproof · cited by 10

Cited by2

Results whose statement or proof uses this declaration.

SSet.Edge.CompStruct.idCompIdproof · cited by 3
SSet.Truncated.Edge.CompStruct.idCompId_simplexstatement and proof · cited by 1