Def Preorder_to_PartialOrder_forget_adjunction

Modification history

2022-02-16 17:16
src/order/category/PartialOrder.lean
feat(order/antisymmetrization): Turning a preorder into a partial order (#11728) …
Added Preorder_to_PartialOrder_forget_adjunctionView on Github →