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

See also

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.

def Prod.Lex.«term_×ₗ_» : Lean.TrailingParserDescr

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

Equations

• Prod.Lex.«term_×ₗ_» = Lean.ParserDescr.trailingNode `Prod.Lex.«term_×ₗ_» 35 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ₗ ") (Lean.ParserDescr.cat `term 34))

instance Prod.Lex.instLE (α : Type u_3) (β : Type u_4) [LT α] [LE β] : LE (Lex (α × β))

Dictionary / lexicographic ordering on pairs.

Equations

• Prod.Lex.instLE α β = { le := Prod.Lex (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 ≤ x2 }

instance Prod.Lex.instLT (α : Type u_3) (β : Type u_4) [LT α] [LT β] : LT (Lex (α × β))

Equations

• Prod.Lex.instLT α β = { lt := Prod.Lex (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }

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.instWellFoundedLTLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (Lex (α × β))

instance Prod.Lex.instWellFoundedRelationLexOfWellFoundedLT {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedRelation (Lex (α × β))

Equations

• Prod.Lex.instWellFoundedRelationLexOfWellFoundedLT = { rel := fun (x1 x2 : Lex (α × β)) => x1 < x2, wf := ⋯ }

instance Prod.Lex.preorder (α : Type u_3) (β : Type u_4) [Preorder α] [Preorder β] : Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

Equations

• Prod.Lex.preorder α β = Preorder.mk ⋯ ⋯ ⋯

theorem Prod.Lex.monotone_fst {α : Type u_1} {β : Type u_2} [Preorder α] [LE β] (t c : Lex (α × β)) (h : t ≤ c) : (ofLex t).1 ≤ (ofLex c).1

theorem Prod.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] : Monotone ⇑toLex

theorem Prod.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] : StrictMono ⇑toLex

instance Prod.Lex.partialOrder (α : Type u_3) (β : Type u_4) [PartialOrder α] [PartialOrder β] : PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

Equations

• Prod.Lex.partialOrder α β = PartialOrder.mk ⋯

instance Prod.Lex.instOrdLexProd {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : Ord (Lex (α × β))

Equations

• Prod.Lex.instOrdLexProd = lexOrd

theorem Prod.Lex.compare_def {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : compare = compareLex (compareOn fun (x : Lex (α × β)) => (ofLex x).1) (compareOn fun (x : Lex (α × β)) => (ofLex x).2)

theorem lexOrd_eq {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] : lexOrd = Prod.Lex.instOrdLexProd

theorem Ord.lex_eq {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] : oα.lex oβ = Prod.Lex.instOrdLexProd

instance Prod.Lex.instOrientedOrdLex {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [Batteries.OrientedOrd α] [Batteries.OrientedOrd β] : Batteries.OrientedOrd (Lex (α × β))

instance Prod.Lex.instTransOrdLex {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] [Batteries.TransOrd α] [Batteries.TransOrd β] : Batteries.TransOrd (Lex (α × β))

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

Dictionary / lexicographic linear order for pairs.

Equations

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

instance Prod.Lex.orderBot {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] : OrderBot (Lex (α × β))

Equations

• Prod.Lex.orderBot = OrderBot.mk ⋯

instance Prod.Lex.orderTop {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] : OrderTop (Lex (α × β))

Equations

• Prod.Lex.orderTop = OrderTop.mk ⋯

instance Prod.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] [BoundedOrder α] [BoundedOrder β] : BoundedOrder (Lex (α × β))

Equations

• Prod.Lex.boundedOrder = BoundedOrder.mk

instance Prod.Lex.instDenselyOrderedLex {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : DenselyOrdered (Lex (α × β))

instance Prod.Lex.noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (Lex (α × β))

instance Prod.Lex.noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (Lex (α × β))

instance Prod.Lex.noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (Lex (α × β))

instance Prod.Lex.noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (Lex (α × β))