Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 17:16 6bcb12c1

View on Github →

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728) Define antisymmetrization, the quotient of a preorder by the "less than both ways" relation. This effectively turns a preorder into a partial order, and this operation is functorial as shown by the new Preorder_to_PartialOrder.

Estimated changes