Some lemmas about lists involving sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Split out from data.list.basic to reduce its dependencies.

theorem list.inj_on_insert_nth_index_of_not_mem {α : Type u_1} (l : list α) (x : α) (hx : x ∉ l) :

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 (λ (a : β) (c : α), f c a) ⊆ set.range (λ (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 (λ (a : β) (c : α), f c a) = set.range (λ (b : γ) (c : α), g c b)) (a : α) :