Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-11 16:26 2ffd72ce

View on Github →

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

Estimated changes

Modified order/basic.lean

added def partial_order.dual

deleted def partial_order_dual

added def preorder.dual

deleted def preorder_dual

Modified order/galois_connection.lean

modified theorem galois_connection.decreasing_l_u

modified theorem galois_connection.increasing_u_l

added def set.kern_image