The lexicographic order on intervals

This order is compatible with the inclusion ordering, but is total.

Under this ordering, [(3, 3), (2, 2), (2, 3), (1, 1), (1, 2), (1, 3)] is sorted.

instance NonemptyInterval.instLELex {α : Type u_1} [LT α] [LE α] : LE (Lex (NonemptyInterval α))

instance NonemptyInterval.instLTLex {α : Type u_1} [LT α] [LE α] : LT (Lex (NonemptyInterval α))

theorem NonemptyInterval.toLex_le_toLex {α : Type u_1} [LT α] [LE α] {x y : NonemptyInterval α} : toLex x ≤ toLex y ↔ y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 ≤ y.toProd.2

theorem NonemptyInterval.toLex_lt_toLex {α : Type u_1} [LT α] [LE α] {x y : NonemptyInterval α} : toLex x < toLex y ↔ y.toProd.1 < x.toProd.1 ∨ x.toProd.1 = y.toProd.1 ∧ x.toProd.2 < y.toProd.2

instance NonemptyInterval.instDecidableLELexOfDecidableEqOfDecidableLT {α : Type u_1} [LT α] [LE α] [DecidableEq α] [DecidableLT α] [DecidableLE α] : DecidableLE (Lex (NonemptyInterval α))

instance NonemptyInterval.instDecidableLTLexOfDecidableEq {α : Type u_1} [LT α] [LE α] [DecidableEq α] [DecidableLT α] : DecidableLT (Lex (NonemptyInterval α))

instance NonemptyInterval.instPreorderLex {α : Type u_1} [Preorder α] : Preorder (Lex (NonemptyInterval α))

theorem NonemptyInterval.toLex_mono {α : Type u_1} [PartialOrder α] : Monotone ⇑toLex

theorem NonemptyInterval.toLex_strictMono {α : Type u_1} [PartialOrder α] : StrictMono ⇑toLex

instance NonemptyInterval.instPartialOrderLex {α : Type u_1} [PartialOrder α] : PartialOrder (Lex (NonemptyInterval α))

instance NonemptyInterval.instLinearOrderLex {α : Type u_1} [LinearOrder α] : LinearOrder (Lex (NonemptyInterval α))