# Documentation

Mathlib.Data.Prod.Lex

# Lexicographic order #

This file defines the lexicographic relation for pairs of orders, partial orders and linear orders.

## Main declarations #

• Prod.Lex.
Order: Instances lifting the orders on α and β to α ×ₗ β.

## Notation #

• α ×ₗ β: α × β equipped with the lexicographic order

Related files are:

• Data.Finset.CoLex: Colexicographic order on finite sets.
• Data.List.Lex: Lexicographic order on lists.
• Data.Pi.Lex: Lexicographic order on Πₗ i, α i.
• Data.PSigma.Order: Lexicographic order on Σ' i, α i.
• Data.Sigma.Order: Lexicographic order on Σ i, α i.

A type synonym to equip a type with its lexicographic order.

Instances For
instance Prod.Lex.decidableEq (α : Type u_4) (β : Type u_5) [] [] :
DecidableEq (Lex (α × β))
instance Prod.Lex.inhabited (α : Type u_4) (β : Type u_5) [] [] :
Inhabited (Lex (α × β))
instance Prod.Lex.instLE (α : Type u_4) (β : Type u_5) [LT α] [LE β] :
LE (Lex (α × β))

Dictionary / lexicographic ordering on pairs.

instance Prod.Lex.instLT (α : Type u_4) (β : Type u_5) [LT α] [LT β] :
LT (Lex (α × β))
theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [LT α] [LE β] (a : α × β) (b : α × β) :
toLex a toLex b a.fst < b.fst a.fst = b.fst a.snd b.snd
theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] (a : α × β) (b : α × β) :
toLex a < toLex b a.fst < b.fst a.fst = b.fst a.snd < b.snd
instance Prod.Lex.preorder (α : Type u_4) (β : Type u_5) [] [] :
Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

theorem Prod.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [] [] :
Monotone toLex
theorem Prod.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [] [] :
StrictMono toLex
instance Prod.Lex.partialOrder (α : Type u_4) (β : Type u_5) [] [] :
PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

instance Prod.Lex.linearOrder (α : Type u_4) (β : Type u_5) [] [] :
LinearOrder (Lex (α × β))

Dictionary / lexicographic linear order for pairs.

instance Prod.Lex.instOrdLexProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
Ord (Lex (α × β))
instance Prod.Lex.orderBot {α : Type u_1} {β : Type u_2} [] [] [] [] :
OrderBot (Lex (α × β))
instance Prod.Lex.orderTop {α : Type u_1} {β : Type u_2} [] [] [] [] :
OrderTop (Lex (α × β))
instance Prod.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [] [] [] [] :
BoundedOrder (Lex (α × β))
instance Prod.Lex.instDenselyOrderedLexProdInstLTToLTToLT {α : Type u_1} {β : Type u_2} [] [] [] [] :
instance Prod.Lex.noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (Lex (α × β))
instance Prod.Lex.noMinOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (Lex (α × β))
instance Prod.Lex.noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (Lex (α × β))
instance Prod.Lex.noMinOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (Lex (α × β))