### Lexicographic ordering #

source
@[simp]
theorem List.lt_toArray {α : Type u_1} [LT α] {l₁ l₂ : List α} :
l₁.toArray < l₂.toArray ↔ l₁ < l₂
source
@[simp]
theorem List.le_toArray {α : Type u_1} [LT α] {l₁ l₂ : List α} :
l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂
source
@[simp]
theorem Array.lt_toList {α : Type u_1} [LT α] {xs ys : Array α} :
xs.toList < ys.toList ↔ xs < ys
source
@[simp]
theorem Array.le_toList {α : Type u_1} [LT α] {xs ys : Array α} :
xs.toList ≤ ys.toList ↔ xs ≤ ys
source
theorem Array.not_lt_iff_ge {α : Type u_1} [LT α] {xs ys : Array α} :
¬xs < ys ↔ ys ≤ xs
source
theorem Array.not_le_iff_gt {α : Type u_1} [LT α] {xs ys : Array α} :
¬xs ≤ ys ↔ ys < xs
source
@[simp]
theorem Array.lex_empty {α : Type u_1} [BEq α] {lt : α → α → Bool} {xs : Array α} :
xs.lex #[] lt = false
source
@[simp]
theorem List.lex_toArray {α : Type u_1} [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt
source
theorem Array.singleton_lex_singleton {α : Type u_1} {a b : α} [BEq α] {lt : α → α → Bool} :
#[a].lex #[b] lt = lt a b
source
@[simp]
theorem Array.lex_toList {α : Type u_1} [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
xs.toList.lex ys.toList lt = xs.lex ys lt
source
instance Array.instIsLinearOrderOfLawfulOrderLT {α : Type u_1} [LT α] [LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] :
Std.IsLinearOrder (Array α)
source
theorem Array.lt_irrefl {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (xs : Array α) :
¬xs < xs
source
instance Array.ltIrrefl {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] :
Std.Irrefl fun (x1 x2 : Array α) => x1 < x2
source
@[simp]
theorem Array.not_lt_empty {α : Type u_1} [LT α] (xs : Array α) :
¬xs < #[]
source
@[simp]
theorem Array.empty_le {α : Type u_1} [LT α] (xs : Array α) :
#[] ≤ xs
source
@[simp]
theorem Array.le_empty {α : Type u_1} [LT α] {xs : Array α} :
xs ≤ #[] ↔ xs = #[]
source
@[simp]
theorem Array.empty_lt_push {α : Type u_1} [LT α] (xs : Array α) (a : α) :
#[] < xs.push a
source
theorem Array.le_refl {α : Type u_1} [LT α] [i₀ : Std.Irrefl fun (x1 x2 : α) => x1 < x2] (xs : Array α) :
xs ≤ xs
source
instance Array.instReflLeOfIrreflLt {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] :
Std.Refl fun (x1 x2 : Array α) => x1 ≤ x2
source
theorem Array.lt_trans {α : Type u_1} [LT α] [i₁ : Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2] {xs ys zs : Array α} (h₁ : xs < ys) (h₂ : ys < zs) :
xs < zs
source
instance Array.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 : Array α) => x1 < x2) (fun (x1 x2 : Array α) => x1 < x2) fun (x1 x2 : Array α) => x1 < x2
Equations

- Array.instTransLt = { trans := ⋯ }

source
theorem Array.lt_of_le_of_lt {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) :
xs < zs
source
@[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
theorem Array.lt_of_le_of_lt' {α : Type u_1} [LT α] [i₁ : Std.Asymm fun (x1 x2 : α) => x1 < x2] [i₂ : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [i₃ : Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2] {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) :
xs < zs
source
theorem Array.le_trans {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) :
xs ≤ zs
source
@[deprecated Array.le_trans (since := "2025-08-01")]
theorem Array.le_trans' {α : Type u_1} [LT α] [i₁ : Std.Asymm fun (x1 x2 : α) => x1 < x2] [i₂ : Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [i₃ : Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2] {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) :
xs ≤ zs
source
instance Array.instTransLeOfLawfulOrderLTOfIsLinearOrder {α : Type u_1} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] :
Trans (fun (x1 x2 : Array α) => x1 ≤ x2) (fun (x1 x2 : Array α) => x1 ≤ x2) fun (x1 x2 : Array α) => x1 ≤ x2
Equations

- Array.instTransLeOfLawfulOrderLTOfIsLinearOrder = { trans := ⋯ }

source
theorem Array.lt_asymm {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] {xs ys : Array α} (h : xs < ys) :
¬ys < xs
source
instance Array.instAsymmLt {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] :
Std.Asymm fun (x1 x2 : Array α) => x1 < x2
source
theorem Array.le_total {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] (xs ys : Array α) :
xs ≤ ys ∨ ys ≤ xs
source
@[simp]
theorem Array.not_lt {α : Type u_1} [LT α] {xs ys : Array α} :
¬xs < ys ↔ ys ≤ xs
source
@[simp]
theorem Array.not_le {α : Type u_1} [LT α] {xs ys : Array α} :
¬ys ≤ xs ↔ xs < ys
source
theorem Array.le_of_lt {α : Type u_1} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] {xs ys : Array α} (h : xs < ys) :
xs ≤ ys
source
theorem Array.le_iff_lt_or_eq {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] {xs ys : Array α} :
xs ≤ ys ↔ xs < ys ∨ xs = ys
source
theorem Array.le_antisymm {α : Type u_1} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {xs ys : Array α} :
xs ≤ ys → ys ≤ xs → xs = ys
source
instance Array.instTotalLeOfAsymmLt {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] :
Std.Total fun (x1 x2 : Array α) => x1 ≤ x2
source
@[simp]
theorem Array.lex_eq_true_iff_lt {α : Type u_1} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
(xs.lex ys fun (x1 x2 : α) => decide (x1 < x2)) = true ↔ xs < ys
source
@[simp]
theorem Array.lex_eq_false_iff_ge {α : Type u_1} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
(xs.lex ys fun (x1 x2 : α) => decide (x1 < x2)) = false ↔ ys ≤ xs
source
instance Array.instDecidableLTOfDecidableEq {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] :
DecidableLT (Array α)
Equations

- xs.instDecidableLTOfDecidableEq ys = decidable_of_iff ((xs.lex ys fun (x1 x2 : α) => decide (x1 < x2)) = true) ⋯

source
instance Array.instDecidableLEOfDecidableEqOfDecidableLT {α : Type u_1} [DecidableEq α] [LT α] [DecidableLT α] :
DecidableLE (Array α)
Equations

- xs.instDecidableLEOfDecidableEqOfDecidableLT ys = decidable_of_iff ((ys.lex xs fun (x1 x2 : α) => decide (x1 < x2)) = false) ⋯

source
theorem Array.lex_eq_true_iff_exists {α : Type u_1} {l₁ l₂ : Array α} [BEq α] (lt : α → α → Bool) :
l₁.lex l₂ lt = true ↔ (l₁.isEqv (l₂.take l₁.size) fun (x1 x2 : α) => x1 == x2) = true ∧ l₁.size < l₂.size ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.size), ∃ (h₂ : i < l₂.size), (∀ (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₁.size`, 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]`

source
theorem Array.lex_eq_false_iff_exists {α : Type u_1} {l₁ l₂ : Array α} [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 (l₁.take l₂.size) fun (x1 x2 : α) => x1 == x2) = true ∨ ∃ (i : Nat), ∃ (h₁ : i < l₁.size), ∃ (h₂ : i < l₂.size), (∀ (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`)

source
theorem Array.lt_iff_exists {α : Type u_1} [LT α] {xs ys : Array α} :
xs < ys ↔ xs = ys.take xs.size ∧ xs.size < ys.size ∨ ∃ (i : Nat), ∃ (h₁ : i < xs.size), ∃ (h₂ : i < ys.size), (∀ (j : Nat) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
source
theorem Array.le_iff_exists {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {xs ys : Array α} :
xs ≤ ys ↔ xs = ys.take xs.size ∨ ∃ (i : Nat), ∃ (h₁ : i < xs.size), ∃ (h₂ : i < ys.size), (∀ (j : Nat) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]
source
theorem Array.append_left_lt {α : Type u_1} [LT α] {xs ys zs : Array α} (h : ys < zs) :
xs ++ ys < xs ++ zs
source
theorem Array.append_left_le {α : Type u_1} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {xs ys zs : Array α} (h : ys ≤ zs) :
xs ++ ys ≤ xs ++ zs
source
theorem Array.le_append_left {α : Type u_1} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {xs ys : Array α} :
xs ≤ xs ++ ys
source
theorem Array.map_lt {α : Type u_1} {β : Type u_2} [LT α] [LT β] {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs < ys) :
map f xs < map f ys
source
theorem Array.map_le {α : Type u_1} {β : Type u_2} [LT α] [LT β] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Std.Asymm fun (x1 x2 : β) => x1 < x2] [Std.Antisymm fun (x1 x2 : β) => ¬x1 < x2] {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs ≤ ys) :
map f xs ≤ map f ys