Theorem SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplex

Modification history

2025-11-17 08:49
Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
feat(AlgebraicTopology): inductive construction of StrictSegal structures (#31250) …
Added SSet.StrictSegalCore.map_mkOfSucc_zero_spineToSimplexView on Github →