Some lemmas about lists involving sets

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

@[simp]

theorem List.setOf_mem_eq_empty_iff {α : Type u_1} {l : List α} : {x : α | x ∈ l} = ∅ ↔ l = []

@[deprecated List.tail_reverse (since := "2024-12-10")]

theorem List.tail_reverse_eq_reverse_dropLast {α : Type u_1} {l : List α} : l.reverse.tail = l.dropLast.reverse

Alias of List.tail_reverse.

theorem List.injOn_insertIdx_index_of_notMem {α : Type u_1} (l : List α) (x : α) (hx : x ∉ l) : Set.InjOn (fun (k : ℕ) => l.insertIdx k x) {n : ℕ | n ≤ l.length}

@[deprecated List.injOn_insertIdx_index_of_notMem (since := "2025-05-23")]

theorem List.injOn_insertIdx_index_of_not_mem {α : Type u_1} (l : List α) (x : α) (hx : x ∉ l) : Set.InjOn (fun (k : ℕ) => l.insertIdx k x) {n : ℕ | n ≤ l.length}

Alias of List.injOn_insertIdx_index_of_notMem.

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 : α) : Set.range (foldr f a) ⊆ Set.range (foldr 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 : α) : Set.range (foldl f a) ⊆ Set.range (foldl g 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 : α) : Set.range (foldr f a) = Set.range (foldr 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 : α) : Set.range (foldl f a) = Set.range (foldl g 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 : σ) : mapAccumr f as s = 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 : σ) : mapAccumr₂ f as bs s = foldr (fun (ab : α × β) (s : σ × List φ) => let r := f ab.1 ab.2 s.1; (r.1, r.2 :: s.2)) (s, []) (as.zip bs)