Definition 1.4.25 (Lexicographical order).  Let S, T be sets, ⪯ be a partial order on S, ⊑ be a partial order on T. We define:
⪯ ∠ ⊑ := [s ⪯ s' and [s ≠ s' or t ⊑ t']](s,t),(s',t') ∈ S×T
Remarks.

This definition constructs a partial order on the Cartesian product of two sets S and T from partial orders on S and T, combining the two partial orders lexicographically. It is used to define multiplication of ordinal numbers (see $../Numbers/Ordinal/product).

References.