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

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.

ink

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

ink

instance Prod.Lex.decidableEq (α : Type u_1) (β : Type u_2) [inst : DecidableEq α] [inst : DecidableEq β] : DecidableEq (Lex (α × β))

Equations

• Prod.Lex.decidableEq α β = instDecidableEqProd

ink

instance Prod.Lex.inhabited (α : Type u_1) (β : Type u_2) [inst : Inhabited α] [inst : Inhabited β] : Inhabited (Lex (α × β))

Equations

• Prod.Lex.inhabited α β = instInhabitedProd

ink

instance Prod.Lex.instLE (α : Type u_1) (β : Type u_2) [inst : LT α] [inst : LE β] : LE (Lex (α × β))

Dictionary / lexicographic ordering on pairs.

Equations

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

ink

instance Prod.Lex.instLT (α : Type u_1) (β : Type u_2) [inst : LT α] [inst : LT β] : LT (Lex (α × β))

Equations

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

ink

theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LE β] (a : α × β) (b : α × β) : ↑toLex a ≤ ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd

ink

theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [inst : LT α] [inst : LT β] (a : α × β) (b : α × β) : ↑toLex a < ↑toLex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd

ink

instance Prod.Lex.preorder (α : Type u_1) (β : Type u_2) [inst : Preorder α] [inst : Preorder β] : Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

Equations

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

ink

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

ink

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

ink

instance Prod.Lex.partialOrder (α : Type u_1) (β : Type u_2) [inst : PartialOrder α] [inst : PartialOrder β] : PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

Equations

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

ink

instance Prod.Lex.linearOrder (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst : LinearOrder β] : LinearOrder (Lex (α × β))

Dictionary / lexicographic linear order for pairs.

Equations

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

ink

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

Equations

• Prod.Lex.orderBot = OrderBot.mk (_ : ∀ (x : Lex (α × β)), ↑toLex ⊥ ≤ ↑toLex x)

ink

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

Equations

• Prod.Lex.orderTop = OrderTop.mk (_ : ∀ (x : Lex (α × β)), ↑toLex x ≤ ↑toLex ⊤)

ink

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

Equations

• Prod.Lex.boundedOrder = let src := Prod.Lex.orderBot; let src_1 := Prod.Lex.orderTop; BoundedOrder.mk

ink

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

Equations

• @Prod.Lex.instDenselyOrderedLexProdInstLTToLTToLT = @Prod.Lex.instDenselyOrderedLexProdInstLTToLTToLT.proof_1

ink

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

Equations

• @Prod.Lex.noMaxOrder_of_left = @Prod.Lex.noMaxOrder_of_left.proof_1

ink

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

Equations

• @Prod.Lex.noMinOrder_of_left = @Prod.Lex.noMinOrder_of_left.proof_1

ink

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

Equations

• @Prod.Lex.noMaxOrder_of_right = @Prod.Lex.noMaxOrder_of_right.proof_1

ink

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

Equations

• @Prod.Lex.noMinOrder_of_right = @Prod.Lex.noMinOrder_of_right.proof_1