Commit 2023-04-28 02:53 cedf2246

View on Github →

feat: port AlgebraicTopology.SimplicialSet (#3689)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialSet.lean

added def SSet.Truncated

added def SSet.asOrderHom

added def SSet.boundary

added def SSet.boundaryInclusion

added def SSet.horn

added def SSet.hornInclusion

added def SSet.sk

added def SSet.standardSimplex

added def SSet

Modified Mathlib/CategoryTheory/Limits/Types.lean