Commit 2025-06-07 20:52 f4848f31

View on Github →

chore(Order): use new ge/gt naming convention - Part 4 (#25572) This PR fixes the naming and statement of transitivity lemmas for ≤ and <. It deprecates gt_of_ge_of_gt and gt_of_gt_of_ge The main changes are in Mathlib.Order.Basic and Mathlib.Order.Defs.PartialOrder

Estimated changes

deleted theorem le_trans'
deleted theorem lt_of_le_of_lt'
deleted theorem lt_of_lt_of_le'
deleted theorem lt_trans'
modified theorem ge_trans
deleted theorem gt_of_ge_of_gt
deleted theorem gt_of_gt_of_ge
modified theorem gt_trans
added theorem lt_of_le_of_lt'
added theorem lt_of_lt_of_le'
modified theorem lt_trans