Lexicographic ordering

@[simp]

theorem Vector.lt_toArray {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : xs.toArray < ys.toArray ↔ xs < ys

@[simp]

theorem Vector.le_toArray {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : xs.toArray ≤ ys.toArray ↔ xs ≤ ys

@[simp]

theorem Vector.lt_toList {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys

@[simp]

theorem Vector.le_toList {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys

@[simp]

theorem Vector.not_lt {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : ¬xs < ys ↔ ys ≤ xs

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

theorem Vector.not_lt_iff_ge {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : ¬xs < ys ↔ ys ≤ xs

@[simp]

theorem Vector.not_le {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : ¬xs ≤ ys ↔ ys < xs

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

theorem Vector.not_le_iff_gt {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : ¬xs ≤ ys ↔ ys < xs

@[simp]

theorem Vector.mk_lt_mk {α : Type u_1} {n : Nat} {data₁ : Array α} {size₁ : data₁.size = n} {data₂ : Array α} {size₂ : data₂.size = n} [LT α] : mk data₁ size₁ < mk data₂ 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 α] : mk data₁ size₁ ≤ mk data₂ size₂ ↔ data₁ ≤ data₂

@[simp]

theorem Vector.mk_lex_mk {α : Type u_1} {n : Nat} [BEq α] {lt : α → α → Bool} {xs ys : Array α} {n₁ : xs.size = n} {n₂ : ys.size = n} : (mk xs n₁).lex (mk ys n₂) lt = xs.lex ys lt

@[simp]

theorem Vector.lex_toArray {α : Type u_1} {n : Nat} [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} : xs.toArray.lex ys.toArray lt = xs.lex ys lt

@[simp]

theorem Vector.lex_toList {α : Type u_1} {n : Nat} [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} : xs.toList.lex ys.toList lt = xs.lex ys lt

@[simp]

theorem Vector.lex_empty {α : Type u_1} [BEq α] {lt : α → α → Bool} (xs : Vector α 0) : xs.lex #v[] lt = false

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

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

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 α] (xs : Vector α 0) : ¬xs < #v[]

@[simp]

theorem Vector.empty_le {α : Type u_1} [LT α] (xs : Vector α 0) : #v[] ≤ xs

@[simp]

theorem Vector.le_empty {α : Type u_1} [LT α] {xs : Vector α 0} : xs ≤ #v[] ↔ xs = #v[]

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

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] {xs ys zs : Vector α n} (h₁ : xs < ys) (h₂ : ys < zs) : xs < zs

@[instance_reducible]

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} [LT α] [LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs

theorem Vector.le_trans {α : Type u_1} {n : Nat} [LT α] [LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] {xs ys zs : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs

@[instance_reducible]

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

Equations

• Vector.instTransLeOfLawfulOrderLTOfIsLinearOrder = { trans := ⋯ }

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

instance Vector.instAsymmLt {α : Type u_1} {n : Nat} [LT α] [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} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] (xs ys : Vector α n) : xs ≤ ys ∨ ys ≤ xs

theorem Vector.le_antisymm {α : Type u_1} {n : Nat} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] {xs ys : Vector α n} (h₁ : xs ≤ ys) (h₂ : ys ≤ xs) : xs = ys

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

instance Vector.instIsLinearOrderOfLawfulOrderLT {α : Type u_1} {n : Nat} [LT α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] : Std.IsLinearOrder (Vector α n)

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

theorem Vector.le_of_lt {α : Type u_1} {n : Nat} [LT α] [i : Std.Asymm fun (x1 x2 : α) => x1 < x2] {xs ys : Vector α n} (h : xs < ys) : xs ≤ ys

theorem Vector.le_iff_lt_or_eq {α : Type u_1} {n : Nat} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {xs ys : Vector α n} : xs ≤ ys ↔ xs < ys ∨ xs = ys

@[simp]

theorem Vector.lex_eq_true_iff_lt {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} : (xs.lex ys fun (x1 x2 : α) => decide (x1 < x2)) = true ↔ xs < ys

@[simp]

theorem Vector.lex_eq_false_iff_ge {α : Type u_1} {n : Nat} [BEq α] [LawfulBEq α] [LT α] [DecidableLT α] {xs ys : Vector α n} : (xs.lex ys fun (x1 x2 : α) => decide (x1 < x2)) = false ↔ ys ≤ xs

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

theorem Vector.lex_eq_true_iff_exists {α : Type u_1} {n : Nat} [BEq α] (lt : α → α → Bool) {xs ys : Vector α n} : xs.lex ys lt = true ↔ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), (xs[j] == ys[j]) = true) ∧ lt xs[i] ys[i] = true

xs is lexicographically less than ys if 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) {xs ys : Vector α n} : xs.lex ys lt = false ↔ (ys.isEqv xs fun (x1 x2 : α) => x1 == x2) = true ∨ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), (xs[j] == ys[j]) = true) ∧ lt ys[i] xs[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₂ 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 Vector.lt_iff_exists {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} : xs < ys ↔ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]

theorem Vector.le_iff_exists {α : Type u_1} {n : Nat} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {xs ys : Vector α n} : xs ≤ ys ↔ xs = ys ∨ ∃ (i : Nat), ∃ (h : i < n), (∀ (j : Nat) (hj : j < i), xs[j] = ys[j]) ∧ xs[i] < ys[i]

theorem Vector.lt_of_getElem_zero {α : Type u_1} {n : Nat} [LT α] {xs ys : Vector α n} (hn : 0 < n) (h : xs[0] < ys[0]) : xs < ys

theorem Vector.append_left_lt {α : Type u_1} {n m : Nat} [LT α] {xs : Vector α n} {ys ys' : Vector α m} (h : ys < ys') : xs ++ ys < xs ++ ys'

theorem Vector.append_left_le {α : Type u_1} {n m : Nat} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {xs : Vector α n} {ys ys' : Vector α m} (h : ys ≤ ys') : xs ++ ys ≤ xs ++ ys'

@[simp]

theorem Vector.append_left_lt_iff {α : Type u_1} {n m : Nat} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (xs : Vector α n) {ys ys' : Vector α m} : xs ++ ys < xs ++ ys' ↔ ys < ys'

@[simp]

theorem Vector.append_left_le_iff {α : Type u_1} {n m : Nat} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] (xs : Vector α n) {ys ys' : Vector α m} : xs ++ ys ≤ xs ++ ys' ↔ ys ≤ ys'

theorem Vector.append_lt_append_iff {α : Type u_1} {n m : Nat} [LT α] {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} : xs₁ ++ ys₁ < xs₂ ++ ys₂ ↔ xs₁ < xs₂ ∨ xs₁ = xs₂ ∧ ys₁ < ys₂

theorem Vector.append_le_append_iff {α : Type u_1} {n m : Nat} [LT α] [Std.Asymm fun (x1 x2 : α) => x1 < x2] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m} : xs₁ ++ ys₁ ≤ xs₂ ++ ys₂ ↔ xs₁ < xs₂ ∨ xs₁ = xs₂ ∧ ys₁ ≤ ys₂

@[simp]

theorem Vector.append_right_lt_iff {α : Type u_1} {n m : Nat} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {xs₁ xs₂ : Vector α n} (ys : Vector α m) : xs₁ ++ ys < xs₂ ++ ys ↔ xs₁ < xs₂

@[simp]

theorem Vector.append_right_le_iff {α : Type u_1} {n m : Nat} [LT α] [Std.Irrefl fun (x1 x2 : α) => x1 < x2] {xs₁ xs₂ : Vector α n} (ys : Vector α m) : xs₁ ++ ys ≤ xs₂ ++ ys ↔ xs₁ ≤ xs₂

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

theorem Vector.map_le {α : Type u_1} {β : Type u_2} {n : Nat} [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] {xs ys : Vector α n} {f : α → β} (w : ∀ (x y : α), x < y → f x < f y) (h : xs ≤ ys) : map f xs ≤ map f ys

theorem Vector.map_lt_map_iff_of_injective {α : Type u_1} {β : Type u_2} {n : Nat} [LT α] [LT β] (f : α → β) (hf : ∀ (a b : α), f a < f b ↔ a < b) (hfinj : Function.Injective f) {xs ys : Vector α n} : map f xs < map f ys ↔ xs < ys

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 Vector.map_lt_map_iff {α : Type u_1} {β : Type u_2} {n : Nat} [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) {xs ys : Vector α n} : map f xs < map f ys ↔ xs < ys

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 Vector.map_le_map_iff_of_injective {α : Type u_1} {β : Type u_2} {n : Nat} [LT α] [LT β] (f : α → β) (hf : ∀ (a b : α), f a < f b ↔ a < b) (hfinj : Function.Injective f) {xs ys : Vector α n} : map f xs ≤ map f ys ↔ xs ≤ ys

theorem Vector.map_le_map_iff {α : Type u_1} {β : Type u_2} {n : Nat} [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) {xs ys : Vector α n} : map f xs ≤ map f ys ↔ xs ≤ ys

theorem Vector.flatMap_lt_flatMap_iff {α : Type u_1} {β : Type u_2} {m n : Nat} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → Vector β m) (hf : ∀ (a b : α), a < b → f a < f b) (hm : 0 < m) {xs ys : Vector α n} : xs.flatMap f < ys.flatMap f ↔ xs < ys

theorem Vector.flatMap_le_flatMap_iff {α : Type u_1} {β : Type u_2} {m n : Nat} [LT α] [Std.Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Std.Asymm fun (x1 x2 : β) => x1 < x2] (f : α → Vector β m) (hf : ∀ (a b : α), a < b → f a < f b) (hm : 0 < m) {xs ys : Vector α n} : xs.flatMap f ≤ ys.flatMap f ↔ xs ≤ ys