# Lemmas about `List.Pairwise` #

source
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`.

source
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]`.

source
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]