Commit 2022-05-15 19:05 4cf20164

View on Github →

feat(order/cover): Covering elements are unique (#14156) In a linear order, there's at most one element covering a and at most one element being covered by a.

Estimated changes

Modified src/order/cover.lean

added theorem covby.ge_of_gt

added theorem covby.le_of_lt

added theorem covby.unique_left

added theorem covby.unique_right

added theorem wcovby.ge_of_gt

added theorem wcovby.le_of_lt