mathlib
3e56439d - chore(data/set/intervals): relax linear_order to preorder in the proofs of `Ixx_eq_empty_iff` (#8071)

Commit
4 years ago
chore(data/set/intervals): relax linear_order to preorder in the proofs of `Ixx_eq_empty_iff` (#8071) The previous formulations of `Ixx_eq_empty(_iff)` are basically a chaining of this formulation plus `not_lt` or `not_le`. But `not_lt` and `not_le` require `linear_order`. Removing them allows relaxing the typeclasses assumptions on `Ixx_eq_empty_iff` and slightly generalising `Ixx_eq_empty`.
Author
Parents
Loading