Mathlib Map

Theorems · Definition · category theory

SimplexCategory.Truncated

ℕ → Type

The truncated simplex category.

Defined in
Mathlib.AlgebraicTopology.SimplexCategory.Defs
Cited by
236 results in Mathlib
Foundations
Depth 30 from the axioms, rests on 255 definitions · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

SSet.Truncated.Edge · cited by 81Truncated.EdgeSSet.Truncated.HomotopyCategory.mk · cited by 37HomotopyCategory.mkSSet.truncation · cited by 34SSet.truncationSSet.Truncated.Edge.CompStruct · cited by 28Edge.CompStructSSet.Truncated.Edge.edge · cited by 27Edge.edgeSSet.Truncated.spine · cited by 24Truncated.spineSSet.Truncated.HomotopyCategory.homMk · cited by 24HomotopyCategory.homMkSimplexCategory.Truncated.inclusion · cited by 22Truncated.inclusionSSet.Truncated.HomotopyCategory.BinaryProduct.inverse · cited by 20BinaryProduct.inverseSSet.Truncated.Edge.id · cited by 20Edge.idSSet.Truncated.Path.arrow · cited by 20Path.arrowSSet.Truncated.Edge.map · cited by 17Edge.mapSSet.Truncated.Edge.tensor · cited by 16Edge.tensorSSet.Truncated.Path.vertex · cited by 16Path.vertexSSet.Truncated.StrictSegal.spineToSimplex · cited by 14StrictSegal.spineToSimplexSimplexCategory · cited by 2204SimplexCategoryCategoryTheory.ObjectProperty.FullSubcategory · cited by 726ObjectProperty.FullSubcat…SimplexCategory.len · cited by 542SimplexCategory.lenSimplexCategory.TruncatedCITED BYCITES

Cites3

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

Cited by385

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 385.