Commit 2025-06-07 10:03 827b149f

View on Github →

chore(Order): use new ge/gt naming convention - Part 1 (#24775) This is the first PR in a sequence of PRs to apply the new naming convention for order lemmas. This PR changes some lemmas that have multiple occurences of lt or le in their name, and where < and ≤ have their arguments swapped in some places. Then those occurrences of < and ≤ are referred to as gt and ge. Names that will be changed by a follow up PR are Ne.lt_or_lt, Ne.not_le_or_not_le, LT.lt.not_le & friends, The first commit is an automatic replacement of lemma names. The second commit adds deprecations for the renamed lemmas. Later commits are manual fixes. This should make it easy to review.

Estimated changes

added theorem LE.le.ge_or_le
added theorem LE.le.ge_or_lt
added theorem LE.le.gt_or_le
deleted theorem LE.le.le_or_le
deleted theorem LE.le.le_or_lt
deleted theorem LE.le.lt_or_le
deleted theorem ge_imp_eq_iff_le_imp_le
deleted theorem le_imp_eq_iff_le_imp_le
deleted theorem lt_iff_not_le
deleted theorem lt_of_not_le
modified theorem lt_update_self_iff
added theorem not_lt_iff_le_imp_ge
deleted theorem not_lt_iff_le_imp_le
modified theorem update_lt_self_iff
modified theorem compare_ge_iff_ge
modified theorem compare_gt_iff_gt
added theorem eq_or_lt_of_not_gt
deleted theorem eq_or_lt_of_not_lt
modified theorem le_of_not_ge
modified theorem le_of_not_gt
deleted theorem le_of_not_le
deleted theorem le_of_not_lt
modified theorem le_or_gt
deleted theorem le_or_lt
modified theorem lt_iff_not_ge
modified theorem lt_of_not_ge
modified theorem lt_or_ge
modified theorem lt_or_gt_of_ne
deleted theorem lt_or_le
modified theorem ne_iff_lt_or_gt
modified theorem not_le
modified theorem le_of_lt
added theorem lt_iff_le_not_ge
deleted theorem lt_iff_le_not_le
modified theorem lt_irrefl
added theorem lt_of_le_not_ge
deleted theorem lt_of_le_not_le
modified theorem not_le_of_gt
deleted theorem not_le_of_lt
modified theorem not_lt_of_ge
deleted theorem not_lt_of_le
modified theorem Set.Iio_True
modified theorem Set.Ioi_False
added theorem IsChain.le_of_not_gt
deleted theorem IsChain.le_of_not_lt
added theorem IsChain.lt_of_not_ge
deleted theorem IsChain.lt_of_not_le