mathlib3 documentation

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 α}, list.lex r list.nil (a :: l)
cons : ∀ {α : Type u} {r : α → α → Prop} {a : α} {l₁ l₂ : list α}, list.lex r l₁ l₂ → list.lex r (a :: l₁) (a :: l₂)
rel : ∀ {α : Type u} {r : α → α → Prop} {a₁ : α} {l₁ : list α} {a₂ : α} {l₂ : list α}, r a₁ a₂ → list.lex r (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} [is_irrefl α r] {a : α} {l₁ l₂ : list α} :

list.lex r (a :: l₁) (a :: l₂) ↔ list.lex r l₁ l₂

@[simp]

theorem list.lex.not_nil_right {α : Type u} (r : α → α → Prop) (l : list α) :

¬list.lex r l list.nil

@[protected, instance]

def list.lex.is_order_connected {α : Type u} (r : α → α → Prop) [is_order_connected α r] [is_trichotomous α r] :

is_order_connected (list α) (list.lex r)

@[protected, instance]

def list.lex.is_trichotomous {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :

is_trichotomous (list α) (list.lex r)

@[protected, instance]

def list.lex.is_asymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :

is_asymm (list α) (list.lex r)

@[protected, instance]

def list.lex.is_strict_total_order {α : Type u} (r : α → α → Prop) [is_strict_total_order α r] :

is_strict_total_order (list α) (list.lex r)

@[protected, instance]

def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α → α → Prop) [decidable_rel r] :

decidable_rel (list.lex r)

Equations

list.lex.decidable_rel r (a :: l₁) (b :: l₂) = decidable_of_iff (r a b ∨ a = b ∧ list.lex r l₁ l₂) _
list.lex.decidable_rel r (hd :: tl) list.nil = decidable.is_false _
list.lex.decidable_rel r list.nil (b :: l₂) = decidable.is_true list.lex.nil
list.lex.decidable_rel r list.nil list.nil = decidable.is_false _

theorem list.lex.append_right {α : Type u} (r : α → α → Prop) {s₁ s₂ : list α} (t : list α) :

list.lex r s₁ s₂ → list.lex r s₁ (s₂ ++ t)

theorem list.lex.append_left {α : Type u} (R : α → α → Prop) {t₁ t₂ : list α} (h : list.lex R t₁ t₂) (s : list α) :

list.lex R (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 α) :

list.lex r l₁ l₂ → list.lex s l₁ l₂

theorem list.lex.to_ne {α : Type u} {l₁ l₂ : list α} :

list.lex ne l₁ l₂ → l₁ ≠ l₂

theorem decidable.list.lex.ne_iff {α : Type u} [decidable_eq α] {l₁ l₂ : list α} (H : l₁.length ≤ l₂.length) :

list.lex ne l₁ l₂ ↔ l₁ ≠ l₂

theorem list.lex.ne_iff {α : Type u} {l₁ l₂ : list α} (H : l₁.length ≤ l₂.length) :

list.lex ne l₁ l₂ ↔ l₁ ≠ l₂

@[protected, instance]

def list.has_lt' {α : Type u} [has_lt α] :

has_lt (list α)

Equations

list.has_lt' = {lt := list.lex has_lt.lt}

theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :

list.nil < a :: l

@[protected, instance]

def list.linear_order {α : Type u} [linear_order α] :

linear_order (list α)

Equations

list.linear_order = linear_order_of_STO (list.lex has_lt.lt)

@[protected, instance]

def list.has_le' {α : Type u} [linear_order α] :

has_le (list α)

Equations

list.has_le' = preorder.to_has_le (list α)