mathlib
de78d424 - feat(order/rel_iso): add `equiv.to_order_iso` (#8482)

Commit

4 years ago

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`.

Author

urkud

Parents