Commit 2025-10-09 13:01 946a8298
View on Github →feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex (#28395)
In this PR, we show that d-dimensional nondegenerate simplices in Δ[n] identify to Fin (d + 1) ↪o Fin (n + 1).
(This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from StdSimplex.lean to Subcomplex.lean.)