The lexicographic order on finite tuples

This file relates Pi.Lex on Fin n → α to the lexicographic order on lists and characterizes it by the first differing coordinate. The order on Fin (n + 1)-tuples compares heads and then tails (Pi.toLex_lt_toLex_iff_succ), so it is the order of the tuples' lists (List.ofFn_lex_lt_iff, List.ofFn_le_ofFn_iff); since the list order is decidable, so is the tuple order (Pi.Lex.decidableLT, Pi.Lex.decidableLE), where mathlib's LinearOrder on Pi.Lex carries only a classical instance. A tuple is lexicographically at most another when every coordinate where it exceeds the other is preceded by one where it falls short (Pi.lex_le_iff_forall), which is to say that it falls short at the first coordinate where they differ (Pi.lex_le_iff_find). Reindexing both tuples along an equivalence transports the index relation (Pi.lex_comp_equiv).

[UPSTREAM] candidates for Mathlib/Order/PiLex.lean and Mathlib/Data/List/OfFn.lean.

theorem Pi.lex_comp_equiv {κ : Type u_1} {ι : Type u_2} {β : Type u_3} (e : κ ≃ ι) (r : κ → κ → Prop) (s : β → β → Prop) (x y : ι → β) : Pi.Lex r (fun {x : κ} => s) (x ∘ ⇑e) (y ∘ ⇑e) ↔ Pi.Lex (fun (i j : ι) => r (e.symm i) (e.symm j)) (fun {x : ι} => s) x y

Reindexing both tuples along an equivalence e : κ ≃ ι transports the index relation of the lexicographic order to its preimage along e.symm.

theorem Pi.toLex_lt_toLex_iff_succ {α : Type u_1} [LinearOrder α] {n : ℕ} (f g : Fin (n + 1) → α) : toLex f < toLex g ↔ f 0 < g 0 ∨ f 0 = g 0 ∧ toLex (Fin.tail f) < toLex (Fin.tail g)

The lexicographic order on Fin (n + 1)-tuples compares heads, then tails.

theorem List.ofFn_lex_lt_iff {α : Type u_1} [LinearOrder α] {n : ℕ} (f g : Fin n → α) : Lex (fun (x1 x2 : α) => x1 < x2) (ofFn f) (ofFn g) ↔ toLex f < toLex g

The lexicographic order on Fin n-tuples is the lexicographic order on their lists.

theorem List.ofFn_lt_ofFn_iff {α : Type u_1} [LinearOrder α] {n : ℕ} (f g : Fin n → α) : ofFn f < ofFn g ↔ toLex f < toLex g

theorem List.ofFn_le_ofFn_iff {α : Type u_1} [LinearOrder α] {n : ℕ} (f g : Fin n → α) : ofFn f ≤ ofFn g ↔ toLex f ≤ toLex g

theorem List.cons_le_cons_iff' {α : Type u_1} [LinearOrder α] {a b : α} {l₁ l₂ : List α} : a :: l₁ ≤ b :: l₂ ↔ a < b ∨ a = b ∧ l₁ ≤ l₂

The lexicographic order on lists compares heads, then tails.

@[instance_reducible]

instance Pi.Lex.decidableLT {α : Type u_1} [LinearOrder α] {n : ℕ} : DecidableLT (Lex (Fin n → α))

< on Lex (Fin n → α) is decided by comparing the tuples' lists.

Equations

• Pi.Lex.decidableLT a b = decidable_of_iff (List.Lex (fun (x1 x2 : α) => x1 < x2) (List.ofFn (ofLex a)) (List.ofFn (ofLex b))) ⋯

@[instance_reducible]

instance Pi.Lex.decidableLE {α : Type u_1} [LinearOrder α] {n : ℕ} : DecidableLE (Lex (Fin n → α))

Equations

• Pi.Lex.decidableLE a b = decidable_of_iff (¬b < a) ⋯

theorem Pi.lex_le_iff_forall {α : Type u_1} [LinearOrder α] {m : ℕ} (A B : Fin m → α) : toLex A ≤ toLex B ↔ ∀ (p : Fin m), B p < A p → ∃ p' < p, A p' < B p'

A tuple is lexicographically at most another iff every coordinate where it strictly exceeds the other is preceded by one where it is strictly below.

theorem Pi.lex_le_iff_find {α : Type u_1} [LinearOrder α] {m : ℕ} (A B : Fin m → α) [DecidablePred fun (i : Fin m) => B i ≠ A i] : toLex A ≤ toLex B ↔ ∀ (he : ∃ (i : Fin m), B i ≠ A i), A (Fin.find (fun (k : Fin m) => B k ≠ A k) he) < B (Fin.find (fun (k : Fin m) => B k ≠ A k) he)

A tuple is lexicographically at most another iff it is strictly below at the first coordinate where they differ, when one exists.