Theorem SSet.Truncated.Edge.CompStruct.nonempty_iff

Modification history

2025-12-02 14:25
Mathlib/AlgebraicTopology/Quasicategory/TwoTruncated.lean
feat(AlgebraicTopology/Quasicategory): define the homotopy category of a 2-truncated quasicategory (#31630) …
Added SSet.Truncated.Edge.CompStruct.nonempty_iffView on Github →