data.set.list

# Lemmas about lists and set.range#

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

In this file we prove lemmas about range of some operations on lists.

theorem set.range_list_map {α : Type u_1} {β : Type u_2} (f : α β) :
= {l : list β | (x : β), x l x
theorem set.range_list_map_coe {α : Type u_1} (s : set α) :
= {l : list α | (x : α), x l x s}
@[simp]
theorem set.range_list_nth_le {α : Type u_1} (l : list α) :
set.range (λ (k : fin l.length), l.nth_le k _) = {x : α | x l}
theorem set.range_list_nth {α : Type u_1} (l : list α) :
= (option.some '' {x : α | x l})
@[simp]
theorem set.range_list_nthd {α : Type u_1} (l : list α) (d : α) :
set.range (λ (n : ), l.nthd n d) = {x : α | x l}
@[simp]
theorem set.range_list_inth {α : Type u_1} [inhabited α] (l : list α) :
= {x : α | x l}
@[protected, instance]
def list.can_lift {α : Type u_1} {β : Type u_2} (c : out_param α)) (p : out_param Prop)) [ β 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