Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-14 18:24 d5c72605

View on Github →

feat(order/monotone): add lemmas about cmp (#14689) Also replace order_dual.cmp_le_flip with lemmas about to_dual and of_dual.

Estimated changes

Modified src/data/ordmap/ordset.lean

Modified src/order/compare.lean

added theorem cmp_le_of_dual

added theorem cmp_le_to_dual

added theorem cmp_of_dual

added theorem cmp_to_dual

added theorem eq_iff_eq_of_cmp_eq_cmp

deleted theorem order_dual.cmp_le_flip

added theorem ordering.compares.cmp_eq

Modified src/order/monotone.lean

added theorem strict_anti.cmp_map_eq

added theorem strict_anti_on.cmp_map_eq

added theorem strict_mono.cmp_map_eq

added theorem strict_mono_on.cmp_map_eq