Lexicographic ordering of lists.

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:

• Mathlib/Combinatorics/Colex.lean: Colexicographic order on finite sets.
• Mathlib/Data/PSigma/Order.lean: Lexicographic order on Σ' i, α i.
• Mathlib/Order/PiLex.lean: Lexicographic order on Πₗ i, α i.
• Mathlib/Data/Sigma/Order.lean: Lexicographic order on Σ i, α i.
• Mathlib/Data/Prod/Lex.lean: Lexicographic order on α × β.

lexicographic ordering

theorem List.lex_cons_iff {α : Type u} {r : α → α → Prop} [Std.Irrefl r] {a : α} {l₁ l₂ : List α} : Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂

theorem List.lex_nil_or_eq_nil {α : Type u} {r : α → α → Prop} (l : List α) : Lex r [] l ∨ l = []

@[simp]

theorem List.lex_singleton_iff {α : Type u} {r : α → α → Prop} (a b : α) : Lex r [a] [b] ↔ r a b

instance List.Lex.isOrderConnected {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [Std.Trichotomous r] : IsOrderConnected (List α) (Lex r)

instance List.Lex.trichotomous {α : Type u} (r : α → α → Prop) [Std.Trichotomous r] : Std.Trichotomous (Lex r)

instance List.Lex.asymm {α : Type u} (r : α → α → Prop) [Std.Asymm r] : Std.Asymm (Lex r)

@[implicit_reducible]

instance List.Lex.decidableRel {α : Type u} [DecidableEq α] (r : α → α → Prop) [DecidableRel r] : DecidableRel (Lex r)

theorem List.Lex.append_right {α : Type u} (r : α → α → Prop) {s₁ s₂ : List α} (t : List α) : Lex r s₁ s₂ → Lex r s₁ (s₂ ++ t)

theorem List.Lex.append_left {α : Type u} (R : α → α → Prop) {t₁ t₂ : List α} (h : Lex R t₁ t₂) (s : 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 α) : Lex r l₁ l₂ → Lex s l₁ l₂

theorem List.Lex.to_ne {α : Type u} {l₁ l₂ : List α} : Lex (fun (x1 x2 : α) => x1 ≠ x2) l₁ l₂ → l₁ ≠ l₂

theorem Decidable.List.Lex.ne_iff {α : Type u} [DecidableEq α] {l₁ 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₁ l₂ : List α} (H : l₁.length ≤ l₂.length) : Lex (fun (x1 x2 : α) => x1 ≠ x2) l₁ l₂ ↔ l₁ ≠ l₂

@[implicit_reducible]

instance List.instLinearOrder {α : Type u} [LinearOrder α] : LinearOrder (List α)

@[implicit_reducible]

instance List.LE' {α : Type u} [LinearOrder α] : LE (List α)

theorem List.lt_iff_lex_lt {α : Type u} [LT α] (l l' : List α) : l.lt l' ↔ Lex (fun (x1 x2 : α) => x1 < x2) l l'

theorem List.head_le_of_lt {α : Type u} [Preorder α] {a a' : α} {l l' : List α} (h : a' :: l' < a :: l) : a' ≤ a

theorem List.head!_le_of_lt {α : Type u} [Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) : l'.head! ≤ l.head!

theorem List.cons_le_cons {α : Type u} [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) : a :: l' ≤ a :: l