mathlib

a1ab984c - feat(data/finset/lattice,order/basic): add lemmas in order_dual, prove dual order exchanges max' and min' (#4715)

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! Co-authored-by: Johan Commelin <johan@commelin.net>