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

source

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

Instances For

source

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 }

source

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 }

source

theorem Prod.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [LT α] [LE β] {x y : α × β} :

toLex x ≤ toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 ≤ y.2

source

theorem Prod.Lex.toLex_lt_toLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] {x y : α × β} :

toLex x < toLex y ↔ x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2

source

theorem Prod.Lex.le_iff {α : Type u_1} {β : Type u_2} [LT α] [LE β] {x y : Lex (α × β)} :

x ≤ y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 ≤ (ofLex y).2

source

theorem Prod.Lex.lt_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {x y : Lex (α × β)} :

x < y ↔ (ofLex x).1 < (ofLex y).1 ∨ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2

source

instance Prod.Lex.instWellFoundedLTLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] :

WellFoundedLT (Lex (α × β))

source

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 := ⋯ }

source

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

Preorder (Lex (α × β))

Dictionary / lexicographic preorder for pairs.

Equations

Prod.Lex.instPreorder α β = { toLE := Prod.Lex.instLE α β, toLT := Prod.Lex.instLT α β, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

source

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

See also monotone_fst_ofLex for a version stated in terms of Monotone.

source

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

Monotone fun (x : Lex (α × β)) => (ofLex x).1

source

theorem Prod.Lex.toLex_covBy_toLex_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a₁ a₂ : α} {b₁ b₂ : β} :

toLex (a₁, b₁) ⋖ toLex (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ ⋖ b₂ ∨ a₁ ⋖ a₂ ∧ IsMax b₁ ∧ IsMin b₂

source

theorem Prod.Lex.covBy_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : Lex (α × β)} :

a ⋖ b ↔ (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ⋖ (ofLex b).2 ∨ (ofLex a).1 ⋖ (ofLex b).1 ∧ IsMax (ofLex a).2 ∧ IsMin (ofLex b).2

source

theorem Prod.Lex.toLex_le_toLex' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α × β} :

toLex x ≤ toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 ≤ y.2)

Variant of Prod.Lex.toLex_le_toLex for partial orders.

source

theorem Prod.Lex.toLex_lt_toLex' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : α × β} :

toLex x < toLex y ↔ x.1 ≤ y.1 ∧ (x.1 = y.1 → x.2 < y.2)

Variant of Prod.Lex.toLex_lt_toLex for partial orders.

source

theorem Prod.Lex.le_iff' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : Lex (α × β)} :

x ≤ y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 ≤ (ofLex y).2)

Variant of Prod.Lex.le_iff for partial orders.

source

theorem Prod.Lex.lt_iff' {α : Type u_1} {β : Type u_2} [PartialOrder α] [Preorder β] {x y : Lex (α × β)} :

x < y ↔ (ofLex x).1 ≤ (ofLex y).1 ∧ ((ofLex x).1 = (ofLex y).1 → (ofLex x).2 < (ofLex y).2)

Variant of Prod.Lex.lt_iff for partial orders.

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.instPartialOrder (α : Type u_3) (β : Type u_4) [PartialOrder α] [PartialOrder β] :

PartialOrder (Lex (α × β))

Dictionary / lexicographic partial order for pairs.

Equations

Prod.Lex.instPartialOrder α β = { toPreorder := Prod.Lex.instPreorder α β, le_antisymm := ⋯ }

source

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

Ord (Lex (α × β))

Equations

Prod.Lex.instOrdLexProd = lexOrd

source

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)

source

theorem lexOrd_eq {α : Type u_1} {β : Type u_2} [Ord α] [Ord β] :

lexOrd = Prod.Lex.instOrdLexProd

source

theorem Ord.lex_eq {α : Type u_1} {β : Type u_2} [oα : Ord α] [oβ : Ord β] :

oα.lex oβ = Prod.Lex.instOrdLexProd

source

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

Batteries.OrientedOrd (Lex (α × β))

source

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

Batteries.TransOrd (Lex (α × β))

source

instance Prod.Lex.instLinearOrder (α : 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.

source

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

OrderBot (Lex (α × β))

Equations

Prod.Lex.orderBot = { bot := toLex ⊥, bot_le := ⋯ }

source

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

OrderTop (Lex (α × β))

Equations

Prod.Lex.orderTop = { top := toLex ⊤, le_top := ⋯ }

source

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

BoundedOrder (Lex (α × β))

Equations

Prod.Lex.boundedOrder = { toOrderTop := Prod.Lex.orderTop, toOrderBot := Prod.Lex.orderBot }

source

instance Prod.Lex.instDenselyOrderedLex {α : 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 (α × β))