# mathlibdocumentation

order.lexicographic

def lex (α : Type u) (β : Type v) :
Type (max u v)

The cartesian product, equipped with the lexicographic order.

Equations
@[protected, instance]
def lex.decidable_eq {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] :
Equations
@[protected, instance]
def lex.inhabited {α : Type u} {β : Type v} [inhabited α] [inhabited β] :
inhabited (lex α β)
Equations
@[protected, instance]
def lex_has_le {α : Type u} {β : Type v} [preorder α] [preorder β] :
has_le (lex α β)

Dictionary / lexicographic ordering on pairs.

Equations
@[protected, instance]
def lex_has_lt {α : Type u} {β : Type v} [preorder α] [preorder β] :
has_lt (lex α β)
Equations
@[protected, instance]
def lex_preorder {α : Type u} {β : Type v} [preorder α] [preorder β] :
preorder (lex α β)

Dictionary / lexicographic preorder for pairs.

Equations
@[protected, instance]
def lex_partial_order {α : Type u} {β : Type v}  :

Dictionary / lexicographic partial_order for pairs.

Equations
@[protected, instance]
def lex_linear_order {α : Type u} {β : Type v} [linear_order α] [linear_order β] :

Dictionary / lexicographic linear_order for pairs.

Equations
@[protected, instance]
def dlex_has_le {α : Type u} {Z : α → Type v} [preorder α] [Π (a : α), preorder (Z a)] :
has_le (Σ' (a : α), Z a)

Dictionary / lexicographic ordering on dependent pairs.

The 'pointwise' partial order prod.has_le doesn't make sense for dependent pairs, so it's safe to mark these as instances here.

Equations
@[protected, instance]
def dlex_has_lt {α : Type u} {Z : α → Type v} [preorder α] [Π (a : α), preorder (Z a)] :
has_lt (Σ' (a : α), Z a)
Equations
@[protected, instance]
def dlex_preorder {α : Type u} {Z : α → Type v} [preorder α] [Π (a : α), preorder (Z a)] :
preorder (Σ' (a : α), Z a)

Dictionary / lexicographic preorder on dependent pairs.

Equations
@[protected, instance]
def dlex_partial_order {α : Type u} {Z : α → Type v} [Π (a : α), partial_order (Z a)] :
partial_order (Σ' (a : α), Z a)

Dictionary / lexicographic partial_order for dependent pairs.

Equations
@[protected, instance]
def dlex_linear_order {α : Type u} {Z : α → Type v} [linear_order α] [Π (a : α), linear_order (Z a)] :
linear_order (Σ' (a : α), Z a)

Dictionary / lexicographic linear_order for pairs.

Equations