Documentation

Init.Data.List.Nat.Pairwise

Lemmas about List.Pairwise #

theorem List.map_getElem_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun (x x_1 : Fin l.length) => x < x_1) 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]
theorem List.map_get_sublist {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun (x x_1 : Fin l.length) => x < x_1) is) :
(List.map l.get is).Sublist l
theorem List.sublist_eq_map_getElem {α : Type u_1} {l : List α} {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 (x x_1 : Fin l.length) => x < x_1) 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]
theorem List.sublist_eq_map_get :
∀ {α : Type u_1} {l' l : List α}, l'.Sublist l∃ (is : List (Fin l.length)), l' = List.map l.get is List.Pairwise (fun (x x_1 : Fin l.length) => x < x_1) 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 < jR l[i] l[j]