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 α))

Equations

• NonemptyInterval.instLELex = { le := fun (x y : Lex (NonemptyInterval α)) => toLex (ofLex x).toDualProd ≤ toLex (ofLex y).toDualProd }

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

Equations

• NonemptyInterval.instLTLex = { lt := fun (x y : Lex (NonemptyInterval α)) => toLex (ofLex x).toDualProd < toLex (ofLex y).toDualProd }

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 α))

Equations

• NonemptyInterval.instDecidableLELexOfDecidableEqOfDecidableLT x✝¹ x✝ = decidable_of_iff' (x✝.toProd.1 < x✝¹.toProd.1 ∨ x✝¹.toProd.1 = x✝.toProd.1 ∧ x✝¹.toProd.2 ≤ x✝.toProd.2) ⋯

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

Equations

• NonemptyInterval.instDecidableLTLexOfDecidableEq x✝¹ x✝ = decidable_of_iff' (x✝.toProd.1 < x✝¹.toProd.1 ∨ x✝¹.toProd.1 = x✝.toProd.1 ∧ x✝¹.toProd.2 < x✝.toProd.2) ⋯

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

Equations

• NonemptyInterval.instPreorderLex = { toLE := NonemptyInterval.instLELex, toLT := NonemptyInterval.instLTLex, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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 α))

Equations

• NonemptyInterval.instPartialOrderLex = { toPreorder := NonemptyInterval.instPreorderLex, le_antisymm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.