Lexicographic ordering

@[simp]

theorem Vector.lt_toArray {α : Type u_1} {n : Nat} [LT α] (l₁ l₂ : Vector α n) : l₁.toArray < l₂.toArray ↔ l₁ < l₂

@[simp]

theorem Vector.le_toArray {α : Type u_1} {n : Nat} [LT α] (l₁ l₂ : Vector α n) : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂

@[simp]

theorem Vector.lt_toList {α : Type u_1} {n : Nat} [LT α] (l₁ l₂ : Vector α n) : l₁.toList < l₂.toList ↔ l₁ < l₂

@[simp]

theorem Vector.le_toList {α : Type u_1} {n : Nat} [LT α] (l₁ l₂ : Vector α n) : l₁.toList ≤ l₂.toList ↔ l₁ ≤ l₂

theorem Vector.not_lt_iff_ge {α : Type u_1} {n : Nat} [LT α] (l₁ l₂ : Vector α n) : ¬l₁ < l₂ ↔ l₂ ≤ l₁

theorem Vector.not_le_iff_gt {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : Vector α n) : ¬l₁ ≤ l₂ ↔ l₂ < l₁

@[simp]

theorem Vector.mk_lt_mk {α : Type u_1} {n : Nat} {data₁ : Array α} {size₁ : data₁.size = n} {data₂ : Array α} {size₂ : data₂.size = n} [LT α] : { toArray := data₁, size_toArray := size₁ } < { toArray := data₂, size_toArray := size₂ } ↔ data₁ < data₂

@[simp]

theorem Vector.mk_le_mk {α : Type u_1} {n : Nat} {data₁ : Array α} {size₁ : data₁.size = n} {data₂ : Array α} {size₂ : data₂.size = n} [LT α] : { toArray := data₁, size_toArray := size₁ } ≤ { toArray := data₂, size_toArray := size₂ } ↔ data₁ ≤ data₂

@[simp]

theorem Vector.mk_lex_mk {α : Type u_1} {n : Nat} [BEq α] (lt : α → α → Bool) {l₁ l₂ : Array α} {n₁ : l₁.size = n} {n₂ : l₂.size = n} : { toArray := l₁, size_toArray := n₁ }.lex { toArray := l₂, size_toArray := n₂ } lt = l₁.lex l₂ lt

@[simp]

theorem Vector.lex_toArray {α : Type u_1} {n : Nat} [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) : l₁.lex l₂.toArray lt = l₁.lex l₂ lt

@[simp]

theorem Vector.lex_toList {α : Type u_1} {n : Nat} [BEq α] (lt : α → α → Bool) (l₁ l₂ : Vector α n) : l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt

@[simp]

theorem Vector.lex_empty {α : Type u_1} [BEq α] {lt : α → α → Bool} (l₁ : Vector α 0) : l₁.lex { toArray := #[], size_toArray := ⋯ } lt = false

@[simp]

theorem Vector.singleton_lex_singleton {α : Type u_1} {a b : α} [BEq α] {lt : α → α → Bool} : { toArray := #[a], size_toArray := ⋯ }.lex { toArray := #[b], size_toArray := ⋯ } lt = lt a b

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

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

@[simp]

theorem Vector.not_lt_empty {α : Type u_1} [LT α] (l : Vector α 0) : ¬l < { toArray := #[], size_toArray := ⋯ }

@[simp]

theorem Vector.empty_le {α : Type u_1} [LT α] (l : Vector α 0) : { toArray := #[], size_toArray := ⋯ } ≤ l

@[simp]

theorem Vector.le_empty {α : Type u_1} [LT α] (l : Vector α 0) : l ≤ { toArray := #[], size_toArray := ⋯ } ↔ l = { toArray := #[], size_toArray := ⋯ }

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

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

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

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

Equations

• Vector.instTransLt = { trans := ⋯ }

theorem Vector.lt_of_le_of_lt {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [i₀ : Std.Irrefl fun (x1 x2 : α) => x1 < x2] [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] {l₁ l₂ l₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃

theorem Vector.le_trans {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2] {l₁ l₂ l₃ : Vector α n} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃

instance Vector.instTransLeOfDecidableEqOfDecidableLTOfIrreflOfAsymmOfAntisymmOfNotLt {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2] : Trans (fun (x1 x2 : Vector α n) => x1 ≤ x2) (fun (x1 x2 : Vector α n) => x1 ≤ x2) fun (x1 x2 : Vector α n) => x1 ≤ x2

Equations

• Vector.instTransLeOfDecidableEqOfDecidableLTOfIrreflOfAsymmOfAntisymmOfNotLt = { trans := ⋯ }

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

instance Vector.instAsymmLtOfDecidableEqOfDecidableLT {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] : Std.Asymm fun (x1 x2 : Vector α n) => x1 < x2

theorem Vector.le_total {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [i : Std.Total fun (x1 x2 : α) => ¬x1 < x2] (l₁ l₂ : Vector α n) : l₁ ≤ l₂ ∨ l₂ ≤ l₁

instance Vector.instTotalLeOfDecidableEqOfDecidableLTOfNotLt {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Total fun (x1 x2 : α) => ¬x1 < x2] : Std.Total fun (x1 x2 : Vector α n) => x1 ≤ x2

@[simp]

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

@[simp]

theorem Vector.not_le {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} : ¬l₂ ≤ l₁ ↔ l₁ < l₂

theorem Vector.le_of_lt {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [i : Std.Total fun (x1 x2 : α) => ¬x1 < x2] {l₁ l₂ : Vector α n} (h : l₁ < l₂) : l₁ ≤ l₂

theorem Vector.le_iff_lt_or_eq {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Std.Total fun (x1 x2 : α) => ¬x1 < x2] {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

@[simp]

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

@[simp]

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

instance Vector.instDecidableLTOfDecidableEq {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Vector α n)

Equations

• l₁.instDecidableLTOfDecidableEq l₂ = decidable_of_iff ((l₁.lex l₂ fun (x1 x2 : α) => decide (x1 < x2)) = true) ⋯

instance Vector.instDecidableLEOfDecidableEqOfDecidableLT {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Vector α n)

Equations

• l₁.instDecidableLEOfDecidableEqOfDecidableLT l₂ = decidable_of_iff ((l₂.lex l₁ fun (x1 x2 : α) => decide (x1 < x2)) = false) ⋯

theorem Vector.lex_eq_true_iff_exists {α : Type u_1} {n : Nat} [BEq α] (lt : α → α → Bool) {l₁ l₂ : Vector α n} : l₁.lex l₂ lt = true ↔ ∃ (i : Nat), ∃ (h : i < n), (∀ (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]

theorem Vector.lex_eq_false_iff_exists {α : Type u_1} {n : Nat} [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₁ l₂ : Vector α n} : l₁.lex l₂ lt = false ↔ (l₂.isEqv l₁ fun (x1 x2 : α) => x1 == x2) = true ∨ ∃ (i : Nat), ∃ (h : i < n), (∀ (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 asymmmetric (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 Vector.lt_iff_exists {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} : l₁ < l₂ ↔ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

theorem Vector.le_iff_exists {α : Type u_1} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ↔ l₁ = l₂ ∨ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

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

theorem Vector.append_left_le {α : Type u_1} {n m : Nat} [DecidableEq α] [LT α] [DecidableLT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ ≤ l₃) : l₁ ++ l₂ ≤ l₁ ++ l₃

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

theorem Vector.map_le {α : Type u_1} {β : Type u_2} {n : Nat} [DecidableEq α] [LT α] [DecidableLT α] [DecidableEq β] [LT β] [DecidableLT β] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Antisymm fun (x1 x2 : α) => ¬x1 < x2] [Std.Irrefl fun (x1 x2 : β) => x1 < x2] [Std.Asymm fun (x1 x2 : β) => x1 < x2] [Std.Antisymm fun (x1 x2 : β) => ¬x1 < x2] {l₁ l₂ : Vector α n} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : l₁ ≤ l₂) : map f l₁ ≤ map f l₂