mathlib

3b19e7ee - feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432)

feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432) We introduce `of_rel_iso_lt` to build an order isomorphism from a relation isomorphism between `(<)` relations. We also add two basic lemmas on `to_rel_iso_lt`.