Commit 2022-11-18 04:44 454d62cf

View on Github →

feat: port Order.Compare (#569) mathlib3 hash: fd47bdf09e90f553519c712378e651975fe8c829

depends on: #568
depends on: #562

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Compare.lean

added theorem Eq.cmp_eq_eq'

added theorem Eq.cmp_eq_eq

added theorem LT.lt.cmp_eq_gt

added theorem LT.lt.cmp_eq_lt

added theorem Ordering.Compares.cmp_eq

added theorem Ordering.Compares.eq_eq

added theorem Ordering.Compares.eq_gt

added theorem Ordering.Compares.eq_lt

added theorem Ordering.Compares.inj

added theorem Ordering.Compares.le_antisymm

added theorem Ordering.Compares.le_total

added theorem Ordering.Compares.ne_gt

added theorem Ordering.Compares.ne_lt

added def Ordering.Compares

added theorem Ordering.Compares_eq

added theorem Ordering.Compares_gt

added theorem Ordering.Compares_lt

added theorem Ordering.compares_iff_of_compares_impl

added theorem Ordering.compares_swap

added theorem Ordering.orElse_eq_lt

added theorem Ordering.swap_eq_iff_eq_swap

added theorem Ordering.swap_orElse

added def cmpLE

added theorem cmpLE_eq_cmp

added theorem cmpLE_swap

added theorem cmpLE_toDual

added theorem cmp_LE_of_dual

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 theorem cmp_ofDual

added theorem cmp_self_eq_eq

added theorem cmp_swap

added theorem cmp_toDual

added theorem eq_iff_eq_of_cmp_eq_cmp

added theorem le_iff_le_of_cmp_eq_cmp

added def linearOrderOfCompares

added theorem lt_iff_lt_of_cmp_eq_cmp

added theorem ofDual_compares_ofDual

added theorem toDual_compares_toDual