Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 13:31 680733c3

View on Github →

feat(order/hom/basic): compl as a dual order isomorphism (#11630)

Estimated changes

added theorem compl_antitone
added theorem compl_strict_anti
added def order_iso.compl