# 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/Data/Finset/Colex.lean`: Colexicographic order on finite sets.
- `Mathlib/Data/PSigma/Order.lean`: Lexicographic order on `Σ' i, α i`.
- `Mathlib/Data/Pi/Lex.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 #

source
theorem List.lex_cons_iff {α : Type u} {r : α → α → Prop} [IsIrrefl α r] {a : α} {l₁ l₂ : List α} :
Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂
source
theorem List.lex_nil_or_eq_nil {α : Type u} {r : α → α → Prop} (l : List α) :
Lex r [] l ∨ l = []
source
@[simp]
theorem List.lex_singleton_iff {α : Type u} {r : α → α → Prop} (a b : α) :
Lex r [a] [b] ↔ r a b
source
instance List.Lex.isOrderConnected {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] :
IsOrderConnected (List α) (Lex r)
source
theorem List.Lex.isOrderConnected.aux {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] (x✝ x✝¹ x✝² : List α) :
Lex r x✝ x✝² → Lex r x✝ x✝¹ ∨ Lex r x✝¹ x✝²
source
instance List.Lex.isTrichotomous {α : Type u} (r : α → α → Prop) [IsTrichotomous α r] :
IsTrichotomous (List α) (Lex r)
source
theorem List.Lex.isTrichotomous.aux {α : Type u} (r : α → α → Prop) [IsTrichotomous α r] (x✝ x✝¹ : List α) :
Lex r x✝ x✝¹ ∨ x✝ = x✝¹ ∨ Lex r x✝¹ x✝
source
instance List.Lex.isAsymm {α : Type u} (r : α → α → Prop) [IsAsymm α r] :
IsAsymm (List α) (Lex r)
source
theorem List.Lex.isAsymm.aux {α : Type u} (r : α → α → Prop) [IsAsymm α r] (x✝ x✝¹ : List α) :
Lex r x✝ x✝¹ → Lex r x✝¹ x✝ → False
source
instance List.Lex.decidableRel {α : Type u} [DecidableEq α] (r : α → α → Prop) [DecidableRel r] :
DecidableRel (Lex r)
Equations

- List.Lex.decidableRel r x✝ [] = isFalse ⋯
- List.Lex.decidableRel r [] (head :: tail) = isTrue ⋯
- List.Lex.decidableRel r (a :: l₁) (b :: l₂) = decidable_of_iff (r a b ∨ a = b ∧ List.Lex r l₁ l₂) ⋯

source
theorem List.Lex.append_right {α : Type u} (r : α → α → Prop) {s₁ s₂ : List α} (t : List α) :
Lex r s₁ s₂ → Lex r s₁ (s₂ ++ t)
source
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₂)
source
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₂
source
theorem List.Lex.to_ne {α : Type u} {l₁ l₂ : List α} :
Lex (fun (x1 x2 : α) => x1 ≠ x2) l₁ l₂ → l₁ ≠ l₂
source
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₂
source
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₂
source
instance List.instLinearOrder {α : Type u} [LinearOrder α] :
LinearOrder (List α)
Equations

- List.instLinearOrder = linearOrderOfSTO (List.Lex fun (x1 x2 : α) => x1 < x2)

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

- List.LE' = List.instLinearOrder.toLE

source
theorem List.lt_iff_lex_lt {α : Type u} [LT α] (l l' : List α) :
l.lt l' ↔ Lex (fun (x1 x2 : α) => x1 < x2) l l'
source
theorem List.head_le_of_lt {α : Type u} [Preorder α] {a a' : α} {l l' : List α} (h : a' :: l' < a :: l) :
a' ≤ a
source
theorem List.head!_le_of_lt {α : Type u} [Preorder α] [Inhabited α] (l l' : List α) (h : l' < l) (hl' : l' ≠ []) :
l'.head! ≤ l.head!
source
theorem List.cons_le_cons {α : Type u} [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) :
a :: l' ≤ a :: l