mathlib documentation

data.list.lex

Lexicographic ordering of lists. #

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

See also order.lexicographic for the lexicographic order on pairs.

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.

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 α) :
@[instance]
def list.lex.is_order_connected {α : Type u} (r : α → α → Prop) [is_order_connected α r] [is_trichotomous α r] :
@[instance]
def list.lex.is_trichotomous {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :
@[instance]
def list.lex.is_asymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :
@[instance]
def list.lex.is_strict_total_order {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] :
@[instance]
def list.lex.decidable_rel {α : Type u} [decidable_eq α] (r : α → α → Prop) [decidable_rel r] :
Equations
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 bs 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₂
@[instance]
def list.has_lt' {α : Type u} [has_lt α] :
Equations
theorem list.nil_lt_cons {α : Type u} [has_lt α] (a : α) (l : list α) :
@[instance]
def list.has_le' {α : Type u} [linear_order α] :
Equations