Lemmas about List.Pairwise

theorem List.map_getElem_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : Pairwise (fun (x1 x2 : Fin l.length) => x1 < x2) is) : (map (fun (x : Fin l.length) => l[x]) is).Sublist l

Given a list is of monotonically increasing indices into l, getting each index produces a sublist of l.

theorem List.sublist_eq_map_getElem {α : Type u_1} {l l' : List α} (h : l'.Sublist l) : ∃ (is : List (Fin l.length)), l' = map (fun (x : Fin l.length) => l[x]) is ∧ Pairwise (fun (x1 x2 : Fin l.length) => x1 < x2) is

Given a sublist l' <+ l, there exists an increasing list of indices is such that l' = is.map fun i => l[i].

theorem List.pairwise_iff_getElem {α : Type u_1} {R : α → α → Prop} {l : List α} : Pairwise R l ↔ ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]

theorem List.pairwise_lt_finRange (n : Nat) : Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (finRange n)

The list List.finRange n is strictly increasing.

theorem List.pairwise_le_finRange (n : Nat) : Pairwise (fun (x1 x2 : Fin n) => x1 ≤ x2) (finRange n)

The list List.finRange n is increasing.

theorem List.nodup_finRange (n : Nat) : (finRange n).Nodup

The list List.finRange n has no duplicate entries.

@[simp]

theorem List.Nodup.idxOf_getElem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} (H : xs.Nodup) (i : Nat) (h : i < xs.length) : idxOf xs[i] xs = i

In a list with no duplicates, idxOf recovers the index of the element at each position.