# Lexicographic order #

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

## Main declarations #

• Prod.Lex.<pre/partial/linear>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.

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

Dictionary / lexicographic ordering on pairs.

Equations
• = { le := Prod.Lex (fun (x x_1 : α) => x < x_1) fun (x x_1 : β) => x x_1 }
instance Prod.Lex.instLT (α : Type u_4) (β : Type u_5) [LT α] [LT β] :
LT (Lex (α × β))
Equations
• = { lt := Prod.Lex (fun (x x_1 : α) => x < x_1) fun (x x_1 : β) => x < x_1 }
theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [LT α] [LE β] (a : α × β) (b : α × β) :
toLex a toLex b a.1 < b.1 a.1 = b.1 a.2 b.2
theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] (a : α × β) (b : α × β) :
toLex a < toLex b a.1 < b.1 a.1 = b.1 a.2 < b.2
instance Prod.Lex.preorder (α : Type u_4) (β : Type u_5) [] [] :
Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

Equations
theorem Prod.Lex.monotone_fst {α : Type u_1} {β : Type u_2} [] [LE β] (t : Lex (α × β)) (c : Lex (α × β)) (h : t c) :
(ofLex t).1 (ofLex c).1
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.

Equations
• = let __src := ;
instance Prod.Lex.linearOrder (α : Type u_4) (β : Type u_5) [] [] :
LinearOrder (Lex (α × β))

Dictionary / lexicographic linear order for pairs.

Equations
• One or more equations did not get rendered due to their size.
instance Prod.Lex.instOrdLex {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :
Ord (Lex (α × β))
Equations
instance Prod.Lex.orderBot {α : Type u_1} {β : Type u_2} [] [] [] [] :
OrderBot (Lex (α × β))
Equations
• Prod.Lex.orderBot =
instance Prod.Lex.orderTop {α : Type u_1} {β : Type u_2} [] [] [] [] :
OrderTop (Lex (α × β))
Equations
• Prod.Lex.orderTop =
instance Prod.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [] [] [] [] :
BoundedOrder (Lex (α × β))
Equations
• Prod.Lex.boundedOrder = let __src := Prod.Lex.orderBot; let __src_1 := Prod.Lex.orderTop; BoundedOrder.mk
instance Prod.Lex.instDenselyOrderedLex {α : Type u_1} {β : Type u_2} [] [] [] [] :
Equations
• =
instance Prod.Lex.noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (Lex (α × β))
Equations
• =
instance Prod.Lex.noMinOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (Lex (α × β))
Equations
• =
instance Prod.Lex.noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (Lex (α × β))
Equations
• =
instance Prod.Lex.noMinOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (Lex (α × β))
Equations
• =