Def CategoryTheory.Functor.toOrderHom

Modification history

2025-07-31 19:24
Mathlib/CategoryTheory/Category/Preorder.lean
feat: basic translations between `X →o Y` and `X ⥤ Y` (#26415) …
Added CategoryTheory.Functor.toOrderHomView on Github →