Commit 2025-10-09 10:11 66ed00a9

View on Github →

feat(AlgebraicTopology): the type of non degenerate simplices of a simplicial set (#28224) In this PR, we introduce the ordered type X.N of nondegenerate simplices in a simplicial set X.

Estimated changes

added theorem SSet.N.cast_eq_self
added theorem SSet.N.dim_le_of_le
added theorem SSet.N.dim_lt_of_lt
added theorem SSet.N.eq_iff
added theorem SSet.N.le_iff
added theorem SSet.N.mk'_surjective
added def SSet.N.mk
added theorem SSet.N.mk_surjective
added structure SSet.N
added theorem SSet.S.existsUnique_n
added theorem SSet.S.subcomplex_toN
added theorem SSet.S.toN_eq_iff