Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 07:33 eb3595ed

View on Github →

move(order/*): move from algebra.order. the files that aren't about algebra (#9562) algebra.order.basic and algebra.order.functions never mention +, - or *. Thus they belong under order.

Estimated changes

deleted theorem cmp_compares
deleted theorem cmp_eq_cmp_symm
deleted theorem cmp_eq_eq_iff
deleted theorem cmp_eq_gt_iff
deleted theorem cmp_eq_lt_iff
deleted def cmp_le
deleted theorem cmp_le_eq_cmp
deleted theorem cmp_le_swap
deleted theorem cmp_self_eq_eq
deleted theorem cmp_swap
deleted theorem eq.not_gt
deleted theorem eq.not_lt
deleted theorem eq.trans_le
deleted theorem eq_iff_le_not_lt
deleted theorem eq_of_forall_ge_iff
deleted theorem eq_of_forall_le_iff
deleted theorem eq_or_lt_of_le
deleted theorem exists_ge_of_linear
deleted theorem forall_lt_iff_le'
deleted theorem forall_lt_iff_le
deleted theorem ge_iff_le
deleted theorem ge_of_eq
deleted theorem gt_iff_lt
deleted theorem has_le.le.le_iff_eq
deleted theorem has_le.le.le_or_le
deleted theorem has_le.le.le_or_lt
deleted theorem has_le.le.lt_iff_ne
deleted theorem has_le.le.lt_or_le
deleted theorem has_le.le.trans_eq
deleted theorem has_lt.lt.lt_or_lt
deleted theorem has_lt.lt.ne'
deleted theorem le_iff_eq_or_lt
deleted theorem le_iff_le_iff_lt_iff_lt
deleted theorem le_iff_le_of_cmp_eq_cmp
deleted theorem le_imp_le_iff_lt_imp_lt
deleted theorem le_implies_le_of_le_of_le
deleted theorem le_of_forall_le'
deleted theorem le_of_forall_le
deleted theorem le_of_forall_lt'
deleted theorem le_of_forall_lt
deleted theorem le_rfl
deleted theorem lt_iff_le_and_ne
deleted theorem lt_iff_lt_of_cmp_eq_cmp
deleted theorem lt_iff_lt_of_le_iff_le'
deleted theorem lt_iff_lt_of_le_iff_le
deleted theorem lt_iff_not_ge'
deleted theorem lt_imp_lt_of_le_imp_le
deleted theorem lt_of_not_ge'
deleted theorem ne.le_iff_lt
deleted theorem ne.lt_or_lt
deleted theorem ne_iff_lt_iff_le
deleted theorem not_le_of_lt
deleted theorem not_lt_iff_eq_or_lt
deleted theorem not_lt_of_le
deleted theorem ordering.compares.eq_eq
deleted theorem ordering.compares.eq_gt
deleted theorem ordering.compares.eq_lt
deleted theorem ordering.compares.inj
deleted theorem ordering.compares.ne_gt
deleted theorem ordering.compares.ne_lt
deleted def ordering.compares
deleted theorem ordering.compares_swap
deleted theorem ordering.or_else_eq_lt
deleted theorem ordering.swap_or_else
added theorem eq.not_gt
added theorem eq.not_lt
added theorem eq.trans_le
added theorem eq_iff_le_not_lt
added theorem eq_of_forall_ge_iff
added theorem eq_of_forall_le_iff
added theorem eq_or_lt_of_le
added theorem exists_ge_of_linear
added theorem forall_lt_iff_le'
added theorem forall_lt_iff_le
added theorem ge_iff_le
added theorem ge_of_eq
added theorem gt_iff_lt
added theorem has_le.le.le_iff_eq
added theorem has_le.le.le_or_le
added theorem has_le.le.le_or_lt
added theorem has_le.le.lt_iff_ne
added theorem has_le.le.lt_or_le
added theorem has_le.le.trans_eq
added theorem has_lt.lt.lt_or_lt
added theorem has_lt.lt.ne'
added theorem le_iff_eq_or_lt
added theorem le_of_forall_le'
added theorem le_of_forall_le
added theorem le_of_forall_lt'
added theorem le_of_forall_lt
added theorem le_rfl
added theorem lt_iff_le_and_ne
added theorem lt_iff_lt_of_le_iff_le
added theorem lt_iff_not_ge'
added theorem lt_imp_lt_of_le_imp_le
added theorem lt_of_not_ge'
modified theorem lt_self_iff_false
added theorem ne.le_iff_lt
added theorem ne.lt_or_lt
added theorem ne_iff_lt_iff_le
added theorem not_le_of_lt
added theorem not_lt_iff_eq_or_lt
added theorem not_lt_of_le
deleted theorem order_dual.cmp_le_flip
deleted theorem order_dual.dual_compares
added theorem cmp_compares
added theorem cmp_eq_cmp_symm
added theorem cmp_eq_eq_iff
added theorem cmp_eq_gt_iff
added theorem cmp_eq_lt_iff
added def cmp_le
added theorem cmp_le_eq_cmp
added theorem cmp_le_swap
added theorem cmp_self_eq_eq
added theorem cmp_swap
added theorem order_dual.cmp_le_flip
added theorem ordering.compares.inj
added theorem ordering.compares_swap
added theorem ordering.or_else_eq_lt
added theorem ordering.swap_or_else