Theorem SSet.stdSimplex.σ_objEquiv_symm_apply

Modification history

2026-03-27 09:21
Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by a homotopy (#33683) …
Added SSet.stdSimplex.σ_objEquiv_symm_applyView on Github →