Def SSet.RelativeMorphism.botEquiv

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.RelativeMorphism.botEquivView on Github →