Commit 2021-08-01 09:36 de78d424
View on Github →feat(order/rel_iso): add equiv.to_order_iso (#8482)
Sometimes it's easier to show monotone e and monotone e.symm than
e x ≤ e y ↔ x ≤ y.
feat(order/rel_iso): add equiv.to_order_iso (#8482)
Sometimes it's easier to show monotone e and monotone e.symm than
e x ≤ e y ↔ x ≤ y.