Theorem OrderHom.uliftRightMap_uliftLeftMap_eq

Modification history

2025-10-28 23:08
Mathlib/Order/Hom/Basic.lean
feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) …
Added OrderHom.uliftRightMap_uliftLeftMap_eqView on Github →