Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:10 c956647c

View on Github →

feat(order/basic): Simple shortcut lemmas (#13421) Add convenience lemmas to make the API a bit more symmetric and easier to translate between transitive and is_trans. Also rename _ge' to _le in lemmas and fix the is_max_ aliases.

Estimated changes

modified theorem nat.lt_of_floor_lt
modified theorem eq.not_gt
modified theorem eq.not_lt
deleted theorem eq.trans_le
modified theorem ge_antisymm
modified theorem ge_iff_le
modified theorem gt_iff_lt
deleted theorem has_le.le.trans_eq
added theorem le_of_eq_of_le'
added theorem le_of_eq_of_le
added theorem le_of_le_of_eq'
added theorem le_of_le_of_eq
modified theorem le_rfl
added theorem le_trans'
deleted theorem lt_iff_not_ge'
added theorem lt_iff_not_le
added theorem lt_of_eq_of_lt'
added theorem lt_of_eq_of_lt
added theorem lt_of_le_of_lt'
added theorem lt_of_le_of_ne'
added theorem lt_of_lt_of_eq'
added theorem lt_of_lt_of_eq
added theorem lt_of_lt_of_le'
deleted theorem lt_of_not_ge'
added theorem lt_of_not_le
modified theorem lt_self_iff_false
added theorem lt_trans'
added theorem ne.lt_of_le'
added theorem ne.lt_of_le
added theorem of_eq
added theorem transitive_ge
added theorem transitive_gt
added theorem transitive_le
added theorem transitive_lt
added theorem transitive_of_trans