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

See also #

Related files are:

lexicographic ordering #

inductive list.lex {α : Type u} (r : α α Prop) :
list α list α Prop

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 α) :
@[protected, instance]
@[protected, instance]
def list.lex.is_trichotomous {α : Type u} (r : α α Prop) [is_trichotomous α r] :
@[protected, instance]
def list.lex.is_asymm {α : Type u} (r : α α Prop) [is_asymm α r] :
@[protected, instance]
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 α] :
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