Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-24 11:50 c0c52abb

View on Github →

feat(order/upper_lower/basic): Linear order (#19068) Upper/lower sets on a linear order themselves form a linear order.

Estimated changes