Documentation

Mathlib.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 #

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
    theorem List.Lex.cons_iff {α : Type u} {r : ααProp} [IsIrrefl α r] {a : α} {l₁ : List α} {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 []
    theorem List.Lex.nil_left_or_eq_nil {α : Type u} {r : ααProp} (l : List α) :
    List.Lex r [] l l = []
    @[simp]
    theorem List.Lex.singleton_iff {α : Type u} {r : ααProp} (a : α) (b : α) :
    List.Lex r [a] [b] r a b
    instance List.Lex.isOrderConnected {α : Type u} (r : ααProp) [IsOrderConnected α r] [IsTrichotomous α r] :
    Equations
    • =
    theorem List.Lex.isOrderConnected.aux {α : Type u} (r : ααProp) [IsOrderConnected α r] [IsTrichotomous α r] :
    ∀ (x x_1 x_2 : List α), List.Lex r x x_2List.Lex r x x_1 List.Lex r x_1 x_2
    instance List.Lex.isTrichotomous {α : Type u} (r : ααProp) [IsTrichotomous α r] :
    Equations
    • =
    theorem List.Lex.isTrichotomous.aux {α : Type u} (r : ααProp) [IsTrichotomous α r] :
    ∀ (x x_1 : List α), List.Lex r x x_1 x = x_1 List.Lex r x_1 x
    instance List.Lex.isAsymm {α : Type u} (r : ααProp) [IsAsymm α r] :
    Equations
    • =
    theorem List.Lex.isAsymm.aux {α : Type u} (r : ααProp) [IsAsymm α r] :
    ∀ (x x_1 : List α), List.Lex r x x_1List.Lex r x_1 xFalse
    @[deprecated]
    instance List.Lex.isStrictTotalOrder {α : Type u} (r : ααProp) [IsStrictTotalOrder α r] :
    Equations
    • =
    instance List.Lex.decidableRel {α : Type u} [DecidableEq α] (r : ααProp) [DecidableRel r] :
    Equations
    theorem List.Lex.append_right {α : Type u} (r : ααProp) {s₁ : List α} {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₁ : List α} {t₂ : List α} (h : List.Lex R t₁ t₂) (s : List α) :
    List.Lex R (s ++ t₁) (s ++ t₂)
    theorem List.Lex.imp {α : Type u} {r : ααProp} {s : ααProp} (H : ∀ (a b : α), r a bs a b) (l₁ : List α) (l₂ : List α) :
    List.Lex r l₁ l₂List.Lex s l₁ l₂
    theorem List.Lex.to_ne {α : Type u} {l₁ : List α} {l₂ : List α} :
    List.Lex (fun (x1 x2 : α) => x1 x2) l₁ l₂l₁ l₂
    theorem Decidable.List.Lex.ne_iff {α : Type u} [DecidableEq α] {l₁ : List α} {l₂ : List α} (H : l₁.length l₂.length) :
    List.Lex (fun (x1 x2 : α) => x1 x2) l₁ l₂ l₁ l₂
    theorem List.Lex.ne_iff {α : Type u} {l₁ : List α} {l₂ : List α} (H : l₁.length l₂.length) :
    List.Lex (fun (x1 x2 : α) => x1 x2) l₁ l₂ l₁ l₂
    instance List.LT' {α : Type u} [LT α] :
    LT (List α)
    Equations
    • List.LT' = { lt := List.Lex fun (x1 x2 : α) => x1 < x2 }
    theorem List.nil_lt_cons {α : Type u} [LT α] (a : α) (l : List α) :
    [] < a :: l
    Equations
    instance List.LE' {α : Type u} [LinearOrder α] :
    LE (List α)
    Equations
    • List.LE' = Preorder.toLE
    theorem List.lt_iff_lex_lt {α : Type u} [LinearOrder α] (l : List α) (l' : List α) :
    l.lt l' List.Lex (fun (x1 x2 : α) => x1 < x2) l l'
    @[simp]
    theorem List.nil_le {α : Type u_1} [LinearOrder α] {l : List α} :
    [] l
    theorem List.head_le_of_lt {α : Type u} [Preorder α] {a : α} {a' : α} {l : List α} {l' : List α} (h : a' :: l' < a :: l) :
    a' a
    theorem List.head!_le_of_lt {α : Type u} [Preorder α] [Inhabited α] (l : List α) (l' : List α) (h : l' < l) (hl' : l' []) :
    l'.head! l.head!
    theorem List.cons_le_cons {α : Type u} [LinearOrder α] (a : α) {l : List α} {l' : List α} (h : l' l) :
    a :: l' a :: l