Finsupp.lex backwards

Stream: maths

[Violeta Hernández]

Am I being dumb, or is Finsupp.lex kind of defined backwards from usual convention?

[Violeta Hernández]

Say I have f g : {0, 1} → ℕ. I'd expect f < g whenever f 1 < g 1, or f 1 = g 1 and f 0 < g 0.

[Violeta Hernández]

If I understand docs#Finsupp.lex_def correctly, the actual condition would be f 0 < g 0 or f 0 = g 0 and f 1 < g 1

[Kevin Buzzard]

ab comes before ba in the dictionary, right? So I'd expect f < g whenever f 0 < g 0, or f 0 = g 0 and f 1 < g 1.

[Violeta Hernández]

Ah, that makes sense. I was thinking in terms of decimal expansions, but those might actually just be backwards from everything else.

[Violeta Hernández]

The issue is that the result I want to prove is about them

[Violeta Hernández]

I think I can just pre-compose my functions with toDual. So in my example, I'd reinterpret f g : {0, 1}ᵒᵈ → ℕ and then everything works

[Antoine Chambert-Loir]

I don't know which definition is the best one, but I observed for #14981, to define the lexicographic order of a multivariate power series, that one needs to switch the order of the variables (take a WellFoundedGT order!), so I agree that it would be more natural to define the other one as docs#Lex.

On the other hand, in mathematics, we use various lexicographic orders on (Fin n) to_0 Nat :

• Lexicographic order on the variables
• Inverse lexicographic order on the variables (that would be RevLex)
• Two variants where we first sort out by degrees, and then take lexicographic or inverse lexicographic order.

Sooner or later, we will need to have them in mathlib.