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

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.

source

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

Lean.TrailingParserDescr

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

Instances For

source

instance Prod.Lex.decidableEq (α : Type u_4) (β : Type u_5) [DecidableEq α] [DecidableEq β] :

DecidableEq (Lex (α × β))

source

instance Prod.Lex.inhabited (α : Type u_4) (β : Type u_5) [Inhabited α] [Inhabited β] :

Inhabited (Lex (α × β))

source

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

LE (Lex (α × β))

Dictionary / lexicographic ordering on pairs.

source

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

LT (Lex (α × β))

source

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

source

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

source

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

Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

source

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

Monotone ↑toLex

source

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

StrictMono ↑toLex

source

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

PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

source

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

LinearOrder (Lex (α × β))

Dictionary / lexicographic linear order for pairs.

source

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

Ord (Lex (α × β))

source

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

OrderBot (Lex (α × β))

source

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

OrderTop (Lex (α × β))

source

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

BoundedOrder (Lex (α × β))

source

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

DenselyOrdered (Lex (α × β))

source

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

NoMaxOrder (Lex (α × β))

source

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

NoMinOrder (Lex (α × β))

source

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

NoMaxOrder (Lex (α × β))

source

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

NoMinOrder (Lex (α × β))