Theorem SSet.mapHomotopyCategory_obj_mk

Modification history

2026-08-19 11:50
Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
feat(AlgebraicTopology/SimplicialSet): induction principle for morphisms of the homotopy category of a simplicial set (#42673)
Added SSet.mapHomotopyCategory_obj_mkView on Github →