Lexicographic ordering

instance List.instLawfulOrderLTOfAsymmLt {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : List α) => x1 < x2] : Std.LawfulOrderLT (List α)

@[simp]

theorem List.lex_lt {α : Type u_1} [LT α] {l₁ l₂ : List α} : Lex (fun (x1 x2 : α) => x1 < x2) l₁ l₂ ↔ l₁ < l₂

@[simp]

theorem List.not_lex_lt {α : Type u_1} [LT α] {l₁ l₂ : List α} : ¬Lex (fun (x1 x2 : α) => x1 < x2) l₁ l₂ ↔ l₂ ≤ l₁

@[simp]

theorem List.not_lt {α : Type u_1} [LT α] {l₁ l₂ : List α} : ¬l₁ < l₂ ↔ l₂ ≤ l₁

@[deprecated List.not_lt (since := "2025-10-26")]

theorem List.not_lt_iff_ge {α : Type u_1} [LT α] {l₁ l₂ : List α} : ¬l₁ < l₂ ↔ l₂ ≤ l₁

@[simp]

theorem List.not_le {α : Type u_1} [LT α] {l₁ l₂ : List α} : ¬l₁ ≤ l₂ ↔ l₂ < l₁

@[deprecated List.not_le (since := "2025-10-26")]

theorem List.not_le_iff_gt {α : Type u_1} [LT α] {l₁ l₂ : List α} : ¬l₁ ≤ l₂ ↔ l₂ < l₁

theorem List.lex_irrefl {α : Type u_1} {r : α → α → Prop} (irrefl : ∀ (x : α), ¬r x x) (l : List α) : ¬Lex r l l

theorem List.lt_irrefl {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (l : List α) : ¬l < l

instance List.ltIrrefl {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] : Std.Irrefl fun (x1 x2 : List α) => x1 < x2

@[simp]

theorem List.not_lex_nil {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {l : List α✝} : ¬Lex r l []

@[simp]

theorem List.not_lt_nil {α : Type u_1} [LT α] (l : List α) : ¬l < []

@[simp]

theorem List.nil_le {α : Type u_1} [LT α] (l : List α) : [] ≤ l

@[simp]

theorem List.not_nil_lex_iff {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {l : List α✝} : ¬Lex r [] l ↔ l = []

@[simp]

theorem List.le_nil {α : Type u_1} [LT α] {l : List α} : l ≤ [] ↔ l = []

@[simp]

theorem List.nil_lex_cons' {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {a : α✝} {l : List α✝} : Lex r [] (a :: l)

@[simp]

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

theorem List.nil_lt_iff {α : Type u_1} [LT α] {l : List α} : [] < l ↔ l ≠ []

theorem List.cons_lex_cons_iff {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {a : α✝} {l₁ : List α✝} {b : α✝} {l₂ : List α✝} : Lex r (a :: l₁) (b :: l₂) ↔ r a b ∨ a = b ∧ Lex r l₁ l₂

theorem List.cons_lt_cons_iff {α : Type u_1} [LT α] {a b : α} {l₁ l₂ : List α} : a :: l₁ < b :: l₂ ↔ a < b ∨ a = b ∧ l₁ < l₂

theorem List.cons_lt_cons_of_lt {α : Type u_1} [LT α] {a b : α} {l₁ l₂ : List α} (h : a < b) : a :: l₁ < b :: l₂

@[simp]

theorem List.cons_lt_cons_self {α : Type u_1} {a : α} [LT α] [i₀ : Std.Irrefl fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} : a :: l₁ < a :: l₂ ↔ l₁ < l₂

theorem List.not_cons_lex_cons_iff {α : Type u_1} {r : α → α → Prop} [DecidableEq α] [DecidableRel r] {a b : α} {l₁ l₂ : List α} : ¬Lex r (a :: l₁) (b :: l₂) ↔ ¬r a b ∧ a ≠ b ∨ ¬r a b ∧ ¬Lex r l₁ l₂

theorem List.cons_le_cons_iff {α : Type u_1} [LT α] [i₁ : Std.Asymm fun (x1 x2 : α) => x1 < x2] [i₂ : Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {a b : α} {l₁ l₂ : List α} : a :: l₁ ≤ b :: l₂ ↔ a < b ∨ a = b ∧ l₁ ≤ l₂

theorem List.not_lt_of_cons_le_cons {α : Type u_1} [LT α] [i₁ : Std.Asymm fun (x1 x2 : α) => x1 < x2] [i₂ : Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬b < a

theorem List.left_le_left_of_cons_le_cons {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : a ≤ b

theorem List.le_of_cons_le_cons {α : Type u_1} [LT α] [i₀ : Std.Irrefl fun (x1 x2 : α) => x1 < x2] [i₁ : Std.Asymm fun (x1 x2 : α) => x1 < x2] [i₂ : Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {a : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ a :: l₂) : l₁ ≤ l₂

theorem List.le_refl {α : Type u_1} [LT α] [i₀ : Std.Irrefl fun (x1 x2 : α) => x1 < x2] (l : List α) : l ≤ l

instance List.instReflLeOfIrreflLt {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] : Std.Refl fun (x1 x2 : List α) => x1 ≤ x2

theorem List.lex_trans {α : Type u_1} {l₁ l₂ l₃ : List α} {r : α → α → Prop} (lt_trans : ∀ {x y z : α}, r x y → r y z → r x z) (h₁ : Lex r l₁ l₂) (h₂ : Lex r l₂ l₃) : Lex r l₁ l₃

theorem List.lt_trans {α : Type u_1} [LT α] [i₁ : Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2] {l₁ l₂ l₃ : List α} (h₁ : l₁ < l₂) (h₂ : l₂ < l₃) : l₁ < l₃

@[instance_reducible]

instance List.instTransLt {α : Type u_1} [LT α] [Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2] : Trans (fun (x1 x2 : List α) => x1 < x2) (fun (x1 x2 : List α) => x1 < x2) fun (x1 x2 : List α) => x1 < x2

Equations

• List.instTransLt = { trans := ⋯ }

theorem List.lt_of_le_of_lt {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃

theorem List.le_trans {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃

@[instance_reducible]

instance List.instTransLeOfIsLinearOrderOfLawfulOrderLT {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] : Trans (fun (x1 x2 : List α) => x1 ≤ x2) (fun (x1 x2 : List α) => x1 ≤ x2) fun (x1 x2 : List α) => x1 ≤ x2

Equations

• List.instTransLeOfIsLinearOrderOfLawfulOrderLT = { trans := ⋯ }

theorem List.lex_asymm {α : Type u_1} {r : α → α → Prop} (h : ∀ {x y : α}, r x y → ¬r y x) {l₁ l₂ : List α} : Lex r l₁ l₂ → ¬Lex r l₂ l₁

theorem List.lt_asymm {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} (h : l₁ < l₂) : ¬l₂ < l₁

instance List.instAsymmLt {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] : Std.Asymm fun (x1 x2 : List α) => x1 < x2

theorem List.not_lex_total {α : Type u_1} {r : α → α → Prop} (h : ∀ (x y : α), ¬r x y ∨ ¬r y x) (l₁ l₂ : List α) : ¬Lex r l₁ l₂ ∨ ¬Lex r l₂ l₁

theorem List.le_total {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁

theorem List.le_total_of_asymm {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁

instance List.instTotalLeOfAsymmLt {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] : Std.Total fun (x1 x2 : List α) => x1 ≤ x2

instance List.instIsLinearOrder {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] : Std.IsLinearOrder (List α)

theorem List.le_of_lt {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂

theorem List.le_iff_lt_or_eq {α : Type u_1} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

theorem List.lex_eq_decide_lex {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] [DecidableEq α] (lt : α → α → Bool) : l₁.lex l₂ lt = decide (Lex (fun (x y : α) => lt x y = true) l₁ l₂)

@[simp]

theorem List.lex_eq_true_iff_lex {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (lt : α → α → Bool) : l₁.lex l₂ lt = true ↔ Lex (fun (x y : α) => lt x y = true) l₁ l₂

Variant of lex_eq_true_iff using an arbitrary comparator.

@[simp]

theorem List.lex_eq_false_iff_not_lex {α : Type u_1} {l₁ l₂ : List α} [BEq α] [LawfulBEq α] (lt : α → α → Bool) : l₁.lex l₂ lt = false ↔ ¬Lex (fun (x y : α) => lt x y = true) l₁ l₂

Variant of lex_eq_false_iff using an arbitrary comparator.

@[simp]

theorem List.lex_eq_true_iff_lt {α : Type u_1} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : (l₁.lex l₂ fun (x1 x2 : α) => decide (x1 < x2)) = true ↔ l₁ < l₂

@[simp]

theorem List.lex_eq_false_iff_ge {α : Type u_1} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} : (l₁.lex l₂ fun (x1 x2 : α) => decide (x1 < x2)) = false ↔ l₂ ≤ l₁

theorem List.lex_eq_true_iff_exists {α : Type u_1} {l₁ l₂ : List α} [BEq α] (lt : α → α → Bool) : l₁.lex l₂ lt = true ↔ (l₁.isEqv (take l₁.length l₂) fun (x1 x2 : α) => x1 == x2) = true ∧ l₁.length < l₂.length ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.length), ∃ (h₂ : i < l₂.length), (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true

l₁ is lexicographically less than l₂ if either

• l₁ is pairwise equivalent under · == · to l₂.take l₁.length, and l₁ is shorter than l₂ or
• there exists an index i such that
  • for all j < i, l₁[j] == l₂[j] and
  • l₁[i] < l₂[i]

theorem List.lex_eq_false_iff_exists {α : Type u_1} {l₁ l₂ : List α} [BEq α] [PartialEquivBEq α] (lt : α → α → Bool) (lt_irrefl : ∀ (x y : α), (x == y) = true → lt x y = false) (lt_asymm : ∀ (x y : α), lt x y = true → lt y x = false) (lt_antisymm : ∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true) : l₁.lex l₂ lt = false ↔ (l₂.isEqv (take l₂.length l₁) fun (x1 x2 : α) => x1 == x2) = true ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.length), ∃ (h₂ : i < l₂.length), (∀ (j : Nat) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true

l₁ is not lexicographically less than l₂ (which you might think of as "l₂ is lexicographically greater than or equal to l₁"") if either

• l₁ is pairwise equivalent under · == · to l₂.take l₁.length or
• there exists an index i such that
  • for all j < i, l₁[j] == l₂[j] and
  • l₂[i] < l₁[i]

This formulation requires that == and lt are compatible in the following senses:

• == is symmetric (we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
• lt is irreflexive with respect to == (i.e. if x == y then lt x y = false
• lt is asymmetric (i.e. lt x y = true → lt y x = false)
• lt is antisymmetric with respect to == (i.e. lt x y = false → lt y x = false → x == y)

theorem List.lt_iff_exists {α : Type u_1} [LT α] {l₁ l₂ : List α} : l₁ < l₂ ↔ l₁ = take l₁.length l₂ ∧ l₁.length < l₂.length ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.length), ∃ (h₂ : i < l₂.length), (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

theorem List.le_iff_exists {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ = take l₁.length l₂ ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.length), ∃ (h₂ : i < l₂.length), (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

theorem List.lt_of_getElem_zero {α : Type u_1} [LT α] {l₁ l₂ : List α} (h₁ : 0 < l₁.length) (h₂ : 0 < l₂.length) (h : l₁[0] < l₂[0]) : l₁ < l₂

theorem List.append_left_lt {α : Type u_1} [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) : l₁ ++ l₂ < l₁ ++ l₃

theorem List.append_left_le {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) : l₁ ++ l₂ ≤ l₁ ++ l₃

theorem List.le_append_left {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} : l₁ ≤ l₁ ++ l₂

theorem List.IsPrefix.le {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁ ≤ l₂

theorem List.append_lt_append_iff_of_length_eq {α : Type u_1} [LT α] {l₁ l₂ l₃ l₄ : List α} (h : l₁.length = l₂.length) : l₁ ++ l₃ < l₂ ++ l₄ ↔ l₁ < l₂ ∨ l₁ = l₂ ∧ l₃ < l₄

theorem List.append_le_append_iff_of_length_eq {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {l₁ l₂ l₃ l₄ : List α} (h : l₁.length = l₂.length) : l₁ ++ l₃ ≤ l₂ ++ l₄ ↔ l₁ < l₂ ∨ l₁ = l₂ ∧ l₃ ≤ l₄

theorem List.append_right_lt_iff_of_length_eq {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} (l₃ : List α) (h : l₁.length = l₂.length) : l₁ ++ l₃ < l₂ ++ l₃ ↔ l₁ < l₂

theorem List.append_right_le_iff_of_length_eq {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {l₁ l₂ : List α} (l₃ : List α) (h : l₁.length = l₂.length) : l₁ ++ l₃ ≤ l₂ ++ l₃ ↔ l₁ ≤ l₂

@[simp]

theorem List.append_left_lt_iff {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (l₁ : List α) {l₂ l₃ : List α} : l₁ ++ l₂ < l₁ ++ l₃ ↔ l₂ < l₃

@[simp]

theorem List.append_left_le_iff {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (l₁ : List α) {l₂ l₃ : List α} : l₁ ++ l₂ ≤ l₁ ++ l₃ ↔ l₂ ≤ l₃

theorem List.append_lt_append_of_lt_of_not_prefix {α : Type u_1} [LT α] {l₁ l₂ l₃ l₄ : List α} (h₁ : l₁ < l₂) (h₂ : ¬l₁ <+: l₂) : l₁ ++ l₃ < l₂ ++ l₄

theorem List.append_lt_append_iff_lt_of_prefix {α : Type u_1} [LT α] {l₁ l₂ l₃ l₄ : List α} (h₁ : l₁ <+: l₂ → l₁ = l₂) (h₂ : l₂ <+: l₁ → l₂ = l₁) : l₁ ++ l₃ < l₂ ++ l₄ ↔ l₁ < l₂ ∨ l₁ = l₂ ∧ l₃ < l₄

theorem List.map_lt {α : Type u_1} {β : Type u_2} [LT α] [LT β] {l₁ l₂ : List α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : l₁ < l₂) : map f l₁ < map f l₂

theorem List.map_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : β) => x1 < x2] [Std.Trichotomous fun (x1 x2 : β) => x1 < x2] {l₁ l₂ : List α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : l₁ ≤ l₂) : map f l₁ ≤ map f l₂

theorem List.map_lt_map_iff_of_injective {α : Type u_1} {β : Type u_2} [LT α] [LT β] (f : α → β) (hf : ∀ (a b : α), f a < f b ↔ a < b) (hfinj : Function.Injective f) {l₁ l₂ : List α} : map f l₁ < map f l₂ ↔ l₁ < l₂

See map_lt_map_iff for a variant with fewer proof obligations for f but with some mild assumptions on the order on α and β.

theorem List.map_lt_map_iff {α : Type u_1} {β : Type u_2} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → β) (hf : ∀ (a b : α), a < b → f a < f b) {l₁ l₂ : List α} : map f l₁ < map f l₂ ↔ l₁ < l₂

See map_lt_map_iff_of_injective for a variant which does not assume anything about the order on α and β, but with more assumptions on f.

theorem List.map_le_map_iff_of_injective {α : Type u_1} {β : Type u_2} [LT α] [LT β] (f : α → β) (hf : ∀ (a b : α), f a < f b ↔ a < b) (hfinj : Function.Injective f) {l₁ l₂ : List α} : map f l₁ ≤ map f l₂ ↔ l₁ ≤ l₂

theorem List.map_le_map_iff {α : Type u_1} {β : Type u_2} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → β) (hf : ∀ (a b : α), a < b → f a < f b) {l₁ l₂ : List α} : map f l₁ ≤ map f l₂ ↔ l₁ ≤ l₂

theorem List.flatMap_lt_flatMap_iff {α : Type u_1} {β : Type u_2} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → List β) (hf : ∀ (a b : α), a < b → f a < f b) (hp : ∀ (a b : α), f a <+: f b → a = b) (hx : ∀ (a : α), f a ≠ []) {l₁ l₂ : List α} : flatMap f l₁ < flatMap f l₂ ↔ l₁ < l₂

theorem List.flatMap_le_flatMap_iff {α : Type u_1} {β : Type u_2} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → List β) (hf : ∀ (a b : α), a < b → f a < f b) (hp : ∀ (a b : α), f a <+: f b → a = b) (hx : ∀ (a : α), f a ≠ []) {l₁ l₂ : List α} : flatMap f l₁ ≤ flatMap f l₂ ↔ l₁ ≤ l₂