Theorem SSet.stdSimplex.subcomplex_hasDimensionLT_of_neq_top

Modification history

2026-04-11 09:33
Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean
feat(AlgebraicTopology/SimplicialSet): more API for the boundary (#37692)
Added SSet.stdSimplex.subcomplex_hasDimensionLT_of_neq_topView on Github →