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]