mathlib documentation

data.list.lex

Lexicographic ordering of lists. #

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

See also #

Related files are:

lexicographic ordering #

source
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.

source
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₂
source
@[simp]
theorem list.lex.not_nil_right {α : Type u} (r : α → α → Prop) (l : list α) :
¬list.lex r l list.nil
source
@[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)
source
@[protected, instance]
def list.lex.is_trichotomous {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :
is_trichotomous (list α) (list.lex r)
source
@[protected, instance]
def list.lex.is_asymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :
is_asymm (list α) (list.lex r)
source
@[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)
source
@[protected, instance]
def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α → α → Prop) [decidable_rel r] :
decidable_rel (list.lex r)
Equations
source
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)
source
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₂)
source
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₂
source
theorem list.lex.to_ne {α : Type u} {l₁ l₂ : list α} :
list.lex ne l₁ l₂ → l₁ ≠ l₂
source
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₂
source
theorem list.lex.ne_iff {α : Type u} {l₁ l₂ : list α} (H : l₁.length ≤ l₂.length) :
list.lex ne l₁ l₂ ↔ l₁ ≠ l₂
source
@[protected, instance]
def list.has_lt' {α : Type u} [has_lt α] :
has_lt (list α)
Equations
source
theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :
list.nil < a :: l
source
@[protected, instance]
def list.linear_order {α : Type u} [linear_order α] :
linear_order (list α)
Equations
source
@[protected, instance]
def list.has_le' {α : Type u} [linear_order α] :
has_le (list α)
Equations