Direct product of posets

Stream: Is there code for X?

[Violeta Hernández]

As the title says

[Violeta Hernández]

There's lexicographic ordering, which is the default, but I can't find the direct product

[Violeta Hernández]

Just as recap: the direct product on α × β is such that (a, b) ≤ (c, d) iff a ≤ c and b ≤ d

[Violeta Hernández]

(in symbols, λ a b : α × β, a.fst ≤ b.fst ∧ a.snd ≤ b.snd)

[Kyle Miller]

I believe that's the default, actually. docs#prod.partial_order

If you want the lexicographic ordering, you have to use lex α β (docs#lex)