The lexicographic order on disjoint-union labels

Plain α ⊕ β carries no linear order in mathlib (only the ⊕ₗ synonym does); the corrected constrained value of a disjUnion needs one for its through-product orientation. This file transports the lexicographic order to the plain sum (left before right) and pins the disjoint-union factorization interface — the multiplicativity of the corrected value, first target of the factorization chain.

@[instance_reducible]

def RS.sumLexLinearOrder (α β : Type) [LinearOrder α] [LinearOrder β] : LinearOrder (α ⊕ β)

The lexicographic linear order on a plain sum type: left before right.

Equations

• RS.sumLexLinearOrder α β = LinearOrder.lift' ⇑toLex ⋯

theorem RS.sumLex_inl_lt_inl_iff {α β : Type} [LinearOrder α] [LinearOrder β] {a a' : α} : Sum.inl a < Sum.inl a' ↔ a < a'

Within the left block the order is the left order.

theorem RS.sumLex_inr_lt_inr_iff {α β : Type} [LinearOrder α] [LinearOrder β] {b b' : β} : Sum.inr b < Sum.inr b' ↔ b < b'

Within the right block, the right order.

theorem RS.sumLex_inl_lt_inr {α β : Type} [LinearOrder α] [LinearOrder β] (a : α) (b : β) : Sum.inl a < Sum.inr b

Every left label precedes every right one.

theorem RS.sumLex_not_inr_lt_inl {α β : Type} [LinearOrder α] [LinearOrder β] (a : α) (b : β) : ¬Sum.inr b < Sum.inl a

And no right label precedes a left one.