Lemmas about List.Pairwise

theorem List.map_getElem_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun (x1 x2 : Fin l.length) => x1 < x2) is) : (List.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.

@[deprecated List.map_getElem_sublist (since := "2024-07-30")]

theorem List.map_get_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun (x1 x2 : Fin l.length) => ↑x1 < ↑x2) is) : (List.map l.get is).Sublist l

theorem List.sublist_eq_map_getElem {α : Type u_1} {l l' : List α} (h : l'.Sublist l) : ∃ (is : List (Fin l.length)), l' = List.map (fun (x : Fin l.length) => l[x]) is ∧ List.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].

@[deprecated List.sublist_eq_map_getElem (since := "2024-07-30")]

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

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