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: Colexicographic order on finite sets.
• Mathlib.Data.PSigma.Order: Lexicographic order on Σ' i, α i.
• Mathlib.Data.Pi.Lex: Lexicographic order on Πₗ i, α i.
• Mathlib.Data.Sigma.Order: Lexicographic order on Σ i, α i.
• Mathlib.Data.Prod.Lex: Lexicographic order on α × β.

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.

• nil: ∀ {α : Type u} {r : α → α → Prop} {a : α} {l : List α}, List.Lex r [] (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₂)

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] : IsOrderConnected (List α) (List.Lex r)

Equations

• (_ : IsOrderConnected (List α) (List.Lex r)) = (_ : IsOrderConnected (List α) (List.Lex r))

theorem List.Lex.isOrderConnected.aux {α : Type u} (r : α → α → Prop) [IsOrderConnected α r] [IsTrichotomous α r] : ∀ (x x_1 x_2 : List α), List.Lex r x x_2 → List.Lex r x x_1 ∨ List.Lex r x_1 x_2

instance List.Lex.isTrichotomous {α : Type u} (r : α → α → Prop) [IsTrichotomous α r] : IsTrichotomous (List α) (List.Lex r)

Equations

• (_ : IsTrichotomous (List α) (List.Lex r)) = (_ : IsTrichotomous (List α) (List.Lex r))

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] : IsAsymm (List α) (List.Lex r)

Equations

• (_ : IsAsymm (List α) (List.Lex r)) = (_ : IsAsymm (List α) (List.Lex r))

theorem List.Lex.isAsymm.aux {α : Type u} (r : α → α → Prop) [IsAsymm α r] : ∀ (x x_1 : List α), List.Lex r x x_1 → List.Lex r x_1 x → False

instance List.Lex.isStrictTotalOrder {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r] : IsStrictTotalOrder (List α) (List.Lex r)

Equations

• (_ : IsStrictTotalOrder (List α) (List.Lex r)) = (_ : IsStrictTotalOrder (List α) (List.Lex r))

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

Equations

• List.Lex.decidableRel r x [] = isFalse (_ : List.Lex r x [] → False)
• List.Lex.decidableRel r [] (b :: l₂) = isTrue (_ : List.Lex r [] (b :: l₂))
• List.Lex.decidableRel r (a :: l₁) (b :: l₂) = decidable_of_iff (r a b ∨ a = b ∧ List.Lex r l₁ l₂) (_ : r a b ∨ a = b ∧ List.Lex r l₁ l₂ ↔ List.Lex r (a :: l₁) (b :: l₂))

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 b → s 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 (x x_1 : α) => x ≠ x_1) l₁ l₂ → l₁ ≠ l₂

theorem Decidable.List.Lex.ne_iff {α : Type u} [DecidableEq α] {l₁ : List α} {l₂ : List α} (H : List.length l₁ ≤ List.length l₂) : List.Lex (fun (x x_1 : α) => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂

theorem List.Lex.ne_iff {α : Type u} {l₁ : List α} {l₂ : List α} (H : List.length l₁ ≤ List.length l₂) : List.Lex (fun (x x_1 : α) => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂

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

Equations

• List.LT' = { lt := List.Lex fun (x x_1 : α) => x < x_1 }

theorem List.nil_lt_cons {α : Type u} [LT α] (a : α) (l : List α) : [] < a :: l

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

Equations

• List.instLinearOrderList = linearOrderOfSTO (List.Lex fun (x x_1 : α) => x < x_1)

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 α) : List.lt l l' ↔ List.Lex (fun (x x_1 : α) => x < x_1) l l'

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

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

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