Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-27 19:53 a1ab984c

View on Github →

feat(data/finset/lattice,order/basic): add lemmas in order_dual, prove dual order exchanges max' and min' (#4715) Introduce functionality to work with order duals and monotone decreasing maps. The pretty part of the code is by Johan Commelin, the ugly part is my own addition!

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.nonempty.map

Modified src/data/finset/lattice.lean

added theorem finset.max'_eq_of_dual_min'

added theorem finset.min'_eq_of_dual_max'

added theorem finset.of_dual_max_eq_min_of_dual

added theorem finset.of_dual_min_eq_max_of_dual

Created src/order/order_dual.lean

added theorem order_dual.le_to_dual

added theorem order_dual.lt_to_dual

added def order_dual.of_dual

added theorem order_dual.of_dual_inj

added theorem order_dual.of_dual_le_of_dual

added theorem order_dual.of_dual_lt_of_dual

added theorem order_dual.of_dual_symm_eq

added theorem order_dual.of_dual_to_dual

added def order_dual.to_dual

added theorem order_dual.to_dual_inj

added theorem order_dual.to_dual_le

added theorem order_dual.to_dual_le_to_dual

added theorem order_dual.to_dual_lt

added theorem order_dual.to_dual_lt_to_dual

added theorem order_dual.to_dual_of_dual

added theorem order_dual.to_dual_symm_eq