Commit 2025-04-06 17:49 1acb3404

View on Github →

chore(Order/Basic): order lemmas according to Preorder/PartialOrder/LinearOrder (#23624) This way, it is much easier to know where to add new lemmas.

Estimated changes

deleted theorem Eq.not_gt
deleted theorem Eq.not_lt
modified theorem LE.le.le_or_le
modified theorem LE.le.le_or_lt
modified theorem LE.le.lt_or_le
modified theorem LT.lt.lt_or_lt
modified theorem LT.lt.ne'
modified theorem LinearOrder.ext
modified theorem LinearOrder.ext_lt
modified theorem Ne.lt_or_lt
modified def Order.Preimage
modified theorem PartialOrder.ext
modified theorem PartialOrder.ext_lt
modified theorem Preorder.ext
modified theorem Preorder.toLE_injective
modified theorem commutative_of_le
modified theorem eq_of_forall_ge_iff
modified theorem eq_of_forall_gt_iff
modified theorem eq_of_forall_le_iff
modified theorem eq_of_forall_lt_iff
modified theorem exists_forall_ge_and
modified theorem exists_ge_of_linear
modified theorem forall_le_iff_ge
modified theorem forall_le_iff_le
modified theorem forall_lt_iff_le'
modified theorem forall_lt_iff_le
modified theorem ge_of_eq
modified theorem le_iff_le_iff_lt_iff_lt
modified theorem le_imp_le_iff_lt_imp_lt
modified theorem le_implies_le_of_le_of_le
modified theorem le_of_forall_ge
modified theorem le_of_forall_le
modified theorem le_of_forall_lt'
modified theorem le_of_forall_lt
modified theorem lt_iff_lt_of_le_iff_le'
modified theorem lt_iff_lt_of_le_iff_le
modified theorem lt_iff_not_le
modified theorem lt_imp_lt_of_le_imp_le
modified theorem lt_of_not_le
modified theorem lt_or_lt_iff_ne
modified theorem lt_self_iff_false
modified theorem max_def'
modified theorem max_def_lt
modified theorem max_rec'
modified theorem max_rec
modified theorem min_def'
modified theorem min_def_lt
modified theorem min_rec'
modified theorem min_rec
modified theorem ne_of_not_le
modified theorem not_lt_iff_eq_or_lt
modified theorem rel_imp_eq_of_rel_imp_le