Lexicographic order #

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

Main declarations #

lex α: A type synonym of α to equip it with its lexicographic order.
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.psigma.order: Lexicographic order on Σ' i, α i.
data.sigma.order: Lexicographic order on Σ i, α i.

source

def lex (α : Type u) :

Type u

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

Equations

lex α = α

source

def to_lex {α : Type u} :

α ≃ lex α

to_lex is the identity function to the lex of a type.

Equations

to_lex = {to_fun := id α, inv_fun := id (lex α), left_inv := _, right_inv := _}

source

def of_lex {α : Type u} :

lex α ≃ α

of_lex is the identity function from the lex of a type.

Equations

of_lex = to_lex.symm

source

@[simp]

theorem to_lex_symm_eq {α : Type u} :

to_lex.symm = of_lex

source

@[simp]

theorem of_lex_symm_eq {α : Type u} :

of_lex.symm = to_lex

source

@[simp]

theorem to_lex_of_lex {α : Type u} (a : lex α) :

⇑to_lex (⇑of_lex a) = a

source

@[simp]

theorem of_lex_to_lex {α : Type u} (a : α) :

⇑of_lex (⇑to_lex a) = a

source

@[simp]

theorem to_lex_inj {α : Type u} {a b : α} :

⇑to_lex a = ⇑to_lex b ↔ a = b

source

@[simp]

theorem of_lex_inj {α : Type u} {a b : lex α} :

⇑of_lex a = ⇑of_lex b ↔ a = b

source

@[protected]

def lex.rec {α : Type u} {β : lex α → Sort u_1} (h : Π (a : α), β (⇑to_lex a)) (a : lex α) :

β a

A recursor for lex. Use as induction x using lex.rec.

Equations

lex.rec h = λ (a : lex α), h (⇑of_lex a)

source

@[protected, instance]

meta def prod.lex.lex.has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :

has_to_format (α ×ₗ β)

source

@[protected, instance]

def prod.lex.decidable_eq (α : Type u_1) (β : Type u_2) [decidable_eq α] [decidable_eq β] :

decidable_eq (α ×ₗ β)

Equations

prod.lex.decidable_eq α β = prod.decidable_eq

source

@[protected, instance]

def prod.lex.inhabited (α : Type u_1) (β : Type u_2) [inhabited α] [inhabited β] :

inhabited (α ×ₗ β)

Equations

prod.lex.inhabited α β = prod.inhabited

source

@[protected, instance]

def prod.lex.has_le (α : Type u_1) (β : Type u_2) [has_lt α] [has_le β] :

has_le (α ×ₗ β)

Dictionary / lexicographic ordering on pairs.

Equations

prod.lex.has_le α β = {le := prod.lex has_lt.lt has_le.le}

source

@[protected, instance]

def prod.lex.has_lt (α : Type u_1) (β : Type u_2) [has_lt α] [has_lt β] :

has_lt (α ×ₗ β)

Equations

prod.lex.has_lt α β = {lt := prod.lex has_lt.lt has_lt.lt}

source

theorem prod.lex.le_iff {α : Type u} {β : Type v} [has_lt α] [has_le β] (a b : α × β) :

⇑to_lex a ≤ ⇑to_lex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd ≤ b.snd

source

theorem prod.lex.lt_iff {α : Type u} {β : Type v} [has_lt α] [has_lt β] (a b : α × β) :

⇑to_lex a < ⇑to_lex b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd

source

@[protected, instance]

def prod.lex.preorder (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :

preorder (α ×ₗ β)

Dictionary / lexicographic preorder for pairs.

Equations

prod.lex.preorder α β = {le := has_le.le (prod.lex.has_le α β), lt := has_lt.lt (prod.lex.has_lt α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[protected, instance]

def prod.lex.partial_order (α : Type u_1) (β : Type u_2) [partial_order α] [partial_order β] :

partial_order (α ×ₗ β)

Dictionary / lexicographic partial_order for pairs.

Equations

prod.lex.partial_order α β = {le := preorder.le (prod.lex.preorder α β), lt := preorder.lt (prod.lex.preorder α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def prod.lex.linear_order (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

linear_order (α ×ₗ β)

Dictionary / lexicographic linear_order for pairs.

Equations

prod.lex.linear_order α β = {le := partial_order.le (prod.lex.partial_order α β), lt := partial_order.lt (prod.lex.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := prod.lex.decidable has_lt.lt has_le.le (λ (a b : β), has_le.le.decidable a b), decidable_eq := prod.lex.decidable_eq α β (λ (a b : β), eq.decidable a b), decidable_lt := prod.lex.decidable has_lt.lt has_lt.lt (λ (a b : β), has_lt.lt.decidable a b), max := max_default (λ (a b : α ×ₗ β), prod.lex.decidable has_lt.lt has_le.le a b), max_def := _, min := min_default (λ (a b : α ×ₗ β), prod.lex.decidable has_lt.lt has_le.le a b), min_def := _}