Skip to main content

OrderIso

structure OrderIso[A: PartialOrder, B: PartialOrder] {
    map: A -> B
    inv: B -> A
} constraint {
    is_order_iso_pair(map, inv)
}

An order isomorphism with explicit inverse data.

GitHub

inv​

OrderIso.inv: (OrderIso[A, B], B) -> A

The inverse order-preserving map.

map​

OrderIso.map: (OrderIso[A, B], A) -> B

The order-preserving map.