mathlib

62d814a4 - refactor(order/lexicographic): Change the `lex` synonym (#10926)

refactor(order/lexicographic): Change the `lex` synonym (#10926) At least five types have a natural lexicographic order, namely: * `α ⊕ β` where everything on the left is smaller than everything on the right * `Σ i, α i` where things are first ordered following `ι`, then following `α i` * `Σ' i, α i` where things are first ordered following `ι`, then following `α i` * `α × β` where things are first ordered following `α`, then following `β` * `finset α`, which is in a specific sene the dual of `finset.colex`. And we could even add `Π i, α i`, `ι →₀ α`, `Π₀ i, α i`, etc... although those haven't come up yet in practice. Hence, we generalize the `lex` synonym away from `prod` to make it a general purpose synonym to equip a type with its lexicographical order. What was `lex α β` now is `α ×ₗ β`. Note that this PR doesn't add any of the aforementioned instances.