Preorder on dfinsupp

Stream: Is there code for X?

[Yaël Dillies]

Where is the preorder on Π₀ i, σ i? dfinsupp.preorder doesn't hit anything.

[Kevin Buzzard]

Should we really be putting orders on products? What's the order on bool -> real? There are two lexes and possibly more.

[Eric Wieser]

We already have the order on finsupp, so the precedent is established

[Eric Wieser]

The order on f g : bool → real is f ff ≤ g ff ∧ f tt ≤ g tt

[Eric Wieser]

Ie the "greatest common order" of all possible lex orders

[Yaël Dillies]

Also, we have docs#sigma.lex.has_le vs docs#sigma.has_le, docs#lex vs docs#prod. The consensus is that lexicographical orders are the optional ones, and should be treated as such.