Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 12:28 3e56439d

View on Github →

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.

Estimated changes

modified theorem set.Icc_eq_empty
modified theorem set.Icc_eq_empty_iff
added theorem set.Icc_eq_empty_of_lt
modified theorem set.Ico_eq_empty
modified theorem set.Ico_eq_empty_iff
added theorem set.Ico_eq_empty_of_le
modified theorem set.Ico_self
modified theorem set.Ioc_eq_empty
added theorem set.Ioc_eq_empty_iff
added theorem set.Ioc_eq_empty_of_le
modified theorem set.Ioc_self
modified theorem set.Ioo_eq_empty
modified theorem set.Ioo_eq_empty_iff
added theorem set.Ioo_eq_empty_of_le
modified theorem set.Ioo_self