mathlib3 documentation

data.list.lemmas

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) :
set.inj_on (λ (k : ), list.insert_nth k x l) {n : | n l.length}
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 : α) :