Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 16:04 ac567902

View on Github →

feat(order/rel_iso): a new definition of order_iso, using preorder instances (#3838) defines (new) order_embedding and order_iso, which map both < and <= replaces existing rel_embedding and rel_iso instances preserving < or <= with the new abbreviations

Estimated changes

modified def setoid.correspondence
modified def con.correspondence
modified def fin.val.rel_embedding
modified def fin_fin.rel_embedding
added def order_embedding
added theorem order_iso.map_bot
added def order_iso.osymm
added def order_iso
deleted theorem rel_iso.map_bot