mathlib3 documentation


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 : α β) :
set.range ( f) = {l : list β | (x : β), x l x set.range f}
theorem set.range_list_map_coe {α : Type u_1} (s : set α) :
set.range ( coe) = {l : list α | (x : α), x l x s}
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 α) :
theorem set.range_list_nthd {α : Type u_1} (l : list α) (d : α) :
set.range (λ (n : ), l.nthd n d) = has_insert.insert d {x : α | x l}
theorem set.range_list_inth {α : Type u_1} [inhabited α] (l : list α) :
@[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 β) ( 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.