Commit 2024-01-09 21:58 316407db

View on Github →

feat(AlgebraicTopology/SimplicialSet): constructors for subfaces (#9363) constructors for subfaces of the standard simplex and horn simplices

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

added def SSet.horn.const

added def SSet.horn.edge

added def SSet.horn.edge₃

added def SSet.horn.primitiveEdge

added def SSet.horn.primitiveTriangle

added theorem SSet.standardSimplex.coe_edge_toOrderHom

added theorem SSet.standardSimplex.coe_triangle_toOrderHom

added def SSet.standardSimplex.const

added theorem SSet.standardSimplex.const_toOrderHom

added def SSet.standardSimplex.edge

added def SSet.standardSimplex.triangle