# Documentation

Mathlib.Data.List.Lemmas

# Some lemmas about lists involving sets #

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

theorem List.range_map {α : Type u_2} {β : Type u_1} (f : αβ) :
= { l | ∀ (x : β), x lx }
theorem List.range_map_coe {α : Type u_1} (s : Set α) :
Set.range (List.map Subtype.val) = { l | ∀ (x : α), x lx s }
instance List.canLift {α : Type u_1} {β : Type u_2} (c : βα) (p : αProp) [inst : CanLift α β c p] :
CanLift (List α) (List β) () fun l => (x : α) → x lp x

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

Equations
• = { prf := (_ : ∀ (l : List α), ((x : α) → x lp x) → y, List.map c y = l) }
theorem List.injOn_insertNth_index_of_not_mem {α : Type u_1} (l : List α) (x : α) (hx : ¬x l) :
Set.InjOn (fun k => ) { n | n }
theorem List.foldr_range_subset_of_range_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : βαα} {g : γαα} (hfg : ) (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 : ) (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 : α) :