data.prod.lex

# Lexicographic order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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.
@[protected, instance]
meta def prod.lex.lex.has_to_format {α : Type u_1} {β : Type u_2}  :
@[protected, instance]
def prod.lex.decidable_eq (α : Type u_1) (β : Type u_2) [decidable_eq α] [decidable_eq β] :
Equations
@[protected, instance]
def prod.lex.inhabited (α : Type u_1) (β : Type u_2) [inhabited α] [inhabited β] :
Equations
@[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
@[protected, instance]
def prod.lex.has_lt (α : Type u_1) (β : Type u_2) [has_lt α] [has_lt β] :
has_lt ×ₗ β)
Equations
theorem prod.lex.le_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_le β] (a b : α × β) :
a.fst < b.fst a.fst = b.fst a.snd b.snd
theorem prod.lex.lt_iff {α : Type u_1} {β : Type u_2} [has_lt α] [has_lt β] (a b : α × β) :
< a.fst < b.fst a.fst = b.fst a.snd < b.snd
@[protected, instance]
def prod.lex.preorder (α : Type u_1) (β : Type u_2) [preorder α] [preorder β] :
preorder ×ₗ β)

Dictionary / lexicographic preorder for pairs.

Equations
theorem prod.lex.to_lex_mono {α : Type u_1} {β : Type u_2} [preorder β] :
theorem prod.lex.to_lex_strict_mono {α : Type u_1} {β : Type u_2} [preorder β] :
@[protected, instance]
def prod.lex.partial_order (α : Type u_1) (β : Type u_2)  :

Dictionary / lexicographic partial_order for pairs.

Equations
@[protected, instance]
def prod.lex.linear_order (α : Type u_1) (β : Type u_2) [linear_order α] [linear_order β] :

Dictionary / lexicographic linear_order for pairs.

Equations
@[protected, instance]
def prod.lex.order_bot {α : Type u_1} {β : Type u_2} [preorder β] [order_bot α] [order_bot β] :
Equations
@[protected, instance]
def prod.lex.order_top {α : Type u_1} {β : Type u_2} [preorder β] [order_top α] [order_top β] :
Equations
@[protected, instance]
def prod.lex.bounded_order {α : Type u_1} {β : Type u_2} [preorder β]  :
Equations
@[protected, instance]
def prod.lex.lex.densely_ordered {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
@[protected, instance]
def prod.lex.no_max_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order α] :
@[protected, instance]
def prod.lex.no_min_order_of_left {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order α] :
@[protected, instance]
def prod.lex.no_max_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_max_order β] :
@[protected, instance]
def prod.lex.no_min_order_of_right {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] [no_min_order β] :