mathlib
ceb13bad - chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778)

Commit

5 years ago

chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778) Also split long lines and lint. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author

urkud

Parents

90abd3bb

mathlib ceb13bad - chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778)

mathlib
ceb13bad - chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778)