mathlib 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.range_map {α : Type u_1} {β : Type u_2} (f : α β) :
set.range (list.map f) = {l : list β | (x : β), x l x set.range f}
theorem list.range_map_coe {α : Type u_1} (s : set α) :
set.range (list.map coe) = {l : list α | (x : α), x l x s}
@[protected, instance]
def list.can_lift {α : Type u_1} {β : Type u_2} (c : out_param α)) (p : out_param Prop)) [can_lift α β c p] :
can_lift (list α) (list β) (list.map c) (λ (l : list α), (x : α), x l p x)

If each element of a list can be lifted to some type, then the whole list can be lifted to this type.

Equations
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 : α) :