Commit 2024-08-22 12:56 3670510b

View on Github →

chore(Order/Defs): Cleanup (#16059)

Estimated changes

deleted theorem not_le_of_lt
deleted theorem not_lt_of_le
modified theorem Decidable.eq_or_lt_of_le
modified theorem Decidable.le_iff_lt_or_eq
modified theorem Decidable.lt_or_eq_of_le
modified theorem compare_eq_iff_eq
modified theorem compare_ge_iff_ge
modified theorem compare_gt_iff_gt
modified theorem compare_iff
modified theorem compare_le_iff_le
modified theorem compare_lt_iff_lt
modified theorem eq_or_lt_of_not_lt
modified theorem ge_trans
modified theorem gt_irrefl
modified theorem gt_of_ge_of_gt
modified theorem gt_of_gt_of_ge
modified theorem gt_trans
modified theorem le_antisymm
modified theorem le_antisymm_iff
modified theorem le_iff_lt_or_eq
modified theorem le_of_eq
modified theorem le_of_eq_or_lt
modified theorem le_of_lt
modified theorem le_of_lt_or_eq
modified theorem le_of_not_ge
modified theorem le_of_not_gt
modified theorem le_of_not_le
modified theorem le_of_not_lt
modified theorem le_or_gt
modified theorem le_or_lt
modified theorem le_refl
modified theorem le_rfl
modified theorem le_total
modified theorem le_trans
modified theorem lt_asymm
modified theorem lt_iff_le_not_le
modified theorem lt_iff_not_ge
modified theorem lt_irrefl
modified theorem lt_of_le_not_le
modified theorem lt_of_le_of_lt
modified theorem lt_of_le_of_ne
modified theorem lt_of_lt_of_le
modified theorem lt_of_not_ge
modified theorem lt_or_eq_of_le
modified theorem lt_or_ge
modified theorem lt_or_gt_of_ne
modified theorem lt_or_le
modified theorem lt_trans
modified theorem lt_trichotomy
modified theorem ne_iff_lt_or_gt
modified theorem ne_of_gt
modified theorem ne_of_lt
modified theorem not_le
modified theorem not_le_of_gt
added theorem not_le_of_lt
modified theorem not_lt
modified theorem not_lt_of_ge
deleted theorem not_lt_of_gt
added theorem not_lt_of_le