Mathlib v3 is deprecated. Go to Mathlib v4

Def partial_order_dual

Modification history

2018-01-11 16:26

order/basic.lean

refactor(order/basic): remove "increasing/decreasing" unusual defs

Deleted partial_order_dual View on Github →

2017-08-10 16:36

algebra/order.lean

construct reals as complete, linear ordered field

Added partial_order_dual View on Github →