Theorem SSet.Truncated.HoRel₂.mk'

Modification history

2025-12-05 11:03
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
refactor(AlgebraicTopology): refactor the homotopy category and the nerve adjunction (#31174) …
Deleted SSet.Truncated.HoRel₂.mk'View on Github →
2025-02-08 20:13
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology): notations X _⦋n⦌ and X ^⦋n⦌ for (co)simplicial objects (#21581) …
Modified SSet.Truncated.HoRel₂.mk'View on Github →
2024-12-20 00:42
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor (#16783) …
Added SSet.Truncated.HoRel₂.mk'View on Github →