data.list.lex

# Lexicographic ordering of lists. #

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

The lexicographic order on list α is defined by L < M iff

• [] < (a :: L) for any a and L,
• (a :: L) < (b :: M) where a < b, or
• (a :: L) < (a :: M) where L < M.

## See also #

Related files are:

• data.finset.colex: Colexicographic order on finite sets.
• data.psigma.order: Lexicographic order on Σ' i, α i.
• data.pi.lex: Lexicographic order on Πₗ i, α i.
• data.sigma.order: Lexicographic order on Σ i, α i.
• data.prod.lex: Lexicographic order on α × β.

### lexicographic ordering #

inductive list.lex {α : Type u} (r : α α Prop) :
list α list α Prop
• nil : {α : Type u} {r : α α Prop} {a : α} {l : list α}, (a :: l)
• cons : {α : Type u} {r : α α Prop} {a : α} {l₁ l₂ : list α}, l₁ l₂ (a :: l₁) (a :: l₂)
• rel : {α : Type u} {r : α α Prop} {a₁ : α} {l₁ : list α} {a₂ : α} {l₂ : list α}, r a₁ a₂ (a₁ :: l₁) (a₂ :: l₂)

Given a strict order < on α, the lexicographic strict order on list α, for which [a0, ..., an] < [b0, ..., b_k] if a0 < b0 or a0 = b0 and [a1, ..., an] < [b1, ..., bk]. The definition is given for any relation r, not only strict orders.

Instances for list.lex
theorem list.lex.cons_iff {α : Type u} {r : α α Prop} [ r] {a : α} {l₁ l₂ : list α} :
(a :: l₁) (a :: l₂) l₁ l₂
@[simp]
theorem list.lex.not_nil_right {α : Type u} (r : α α Prop) (l : list α) :
@[protected, instance]
def list.lex.is_order_connected {α : Type u} (r : α α Prop) [ r] [ r] :
@[protected, instance]
def list.lex.is_trichotomous {α : Type u} (r : α α Prop) [ r] :
@[protected, instance]
def list.lex.is_asymm {α : Type u} (r : α α Prop) [ r] :
@[protected, instance]
def list.lex.is_strict_total_order {α : Type u} (r : α α Prop)  :
@[protected, instance]
def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α α Prop)  :
Equations
theorem list.lex.append_right {α : Type u} (r : α α Prop) {s₁ s₂ : list α} (t : list α) :
s₁ s₂ s₁ (s₂ ++ t)
theorem list.lex.append_left {α : Type u} (R : α α Prop) {t₁ t₂ : list α} (h : t₁ t₂) (s : list α) :
(s ++ t₁) (s ++ t₂)
theorem list.lex.imp {α : Type u} {r s : α α Prop} (H : (a b : α), r a b s a b) (l₁ l₂ : list α) :
l₁ l₂ l₁ l₂
theorem list.lex.to_ne {α : Type u} {l₁ l₂ : list α} :
l₁ l₂ l₁ l₂
theorem decidable.list.lex.ne_iff {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (H : l₁.length l₂.length) :
l₁ l₂ l₁ l₂
theorem list.lex.ne_iff {α : Type u} {l₁ l₂ : list α} (H : l₁.length l₂.length) :
l₁ l₂ l₁ l₂
@[protected, instance]
def list.has_lt' {α : Type u} [has_lt α] :
Equations
theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :
@[protected, instance]
Equations
@[protected, instance]
def list.has_le' {α : Type u} [linear_order α] :
Equations