Documentation

Mathlib.Data.List.Lemmas

Some lemmas about lists involving sets #

Split out from Data.List.Basic to reduce its dependencies.

@[simp]
theorem List.length_flatMap {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
(l.flatMap f).length = (List.map (List.length f) l).sum
theorem List.countP_flatMap {α : Type u_1} {β : Type u_2} (p : βBool) (l : List α) (f : αList β) :
List.countP p (l.flatMap f) = (List.map (List.countP p f) l).sum
theorem List.count_flatMap {α : Type u_1} {β : Type u_2} [BEq β] (l : List α) (f : αList β) (x : β) :
List.count x (l.flatMap f) = (List.map (List.count x f) l).sum
@[deprecated List.getElem_reverse]
theorem List.getElem_reverse' {α : Type u_1} {l : List α} {i : } (h : i < l.reverse.length) :
l.reverse[i] = l[l.length - 1 - i]

Alias of List.getElem_reverse.

@[deprecated List.tail_reverse]
theorem List.tail_reverse_eq_reverse_dropLast {α : Type u_1} (l : List α) :
l.reverse.tail = l.dropLast.reverse

Alias of List.tail_reverse.

@[deprecated List.getElem_tail]
theorem List.nthLe_tail {α : Type u_1} (l : List α) (i : ) (h : i < l.tail.length) :
l.tail[i] = l[i + 1]

Alias of List.getElem_tail.

theorem List.injOn_insertIdx_index_of_not_mem {α : Type u_1} (l : List α) (x : α) (hx : xl) :
Set.InjOn (fun (k : ) => List.insertIdx k x l) {n : | n l.length}
@[deprecated List.injOn_insertIdx_index_of_not_mem]
theorem List.injOn_insertNth_index_of_not_mem {α : Type u_1} (l : List α) (x : α) (hx : xl) :
Set.InjOn (fun (k : ) => List.insertIdx k x l) {n : | n l.length}

Alias of List.injOn_insertIdx_index_of_not_mem.

theorem List.foldr_range_subset_of_range_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βαα} {g : γαα} (hfg : Set.range f Set.range g) (a : α) :
theorem List.foldl_range_subset_of_range_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβα} {g : αγα} (hfg : (Set.range fun (a : β) (c : α) => f c a) Set.range fun (b : γ) (c : α) => g c b) (a : α) :
theorem List.foldr_range_eq_of_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βαα} {g : γαα} (hfg : Set.range f = Set.range g) (a : α) :
theorem List.foldl_range_eq_of_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβα} {g : αγα} (hfg : (Set.range fun (a : β) (c : α) => f c a) = Set.range fun (b : γ) (c : α) => g c b) (a : α) :

MapAccumr and Foldr #

Some lemmas relation mapAccumr and foldr

theorem List.mapAccumr_eq_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} (f : ασσ × β) (as : List α) (s : σ) :
List.mapAccumr f as s = List.foldr (fun (a : α) (s : σ × List β) => let r := f a s.1; (r.1, r.2 :: s.2)) (s, []) as
theorem List.mapAccumr₂_eq_foldr {α : Type u_1} {β : Type u_2} {σ : Type u_4} {φ : Type u_5} (f : αβσσ × φ) (as : List α) (bs : List β) (s : σ) :
List.mapAccumr₂ f as bs s = List.foldr (fun (ab : α × β) (s : σ × List φ) => let r := f ab.1 ab.2 s.1; (r.1, r.2 :: s.2)) (s, []) (as.zip bs)