Theorem SSet.Homotopy.h₀

Modification history

2026-03-27 09:21
Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean
feat(AlgebraicTopology/SimplicialSet): the simplicial homotopy induced by a homotopy (#33683) …
Added SSet.Homotopy.h₀View on Github →