# Documentation

Mathlib.Data.Set.List

# Lemmas about Lists and Set.range#

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 | ∀ (x : β), x lx }
theorem Set.range_list_map_coe {α : Type u_1} (s : Set α) :
Set.range (List.map Subtype.val) = {l | ∀ (x : α), x lx s}
@[simp]
theorem Set.range_list_nthLe {α : Type u_1} (l : List α) :
(Set.range fun k => List.nthLe l k (_ : k < )) = {x | x l}
theorem Set.range_list_get? {α : Type u_1} (l : List α) :
= insert none (some '' {x | x l})
@[simp]
theorem Set.range_list_getD {α : Type u_1} (l : List α) (d : α) :
(Set.range fun n => List.getD l n d) = insert d {x | x l}
@[simp]
theorem Set.range_list_getI {α : Type u_1} [] (l : List α) :
= insert default {x | x l}
instance List.canLift {α : Type u_1} {β : Type u_2} (c : βα) (p : αProp) [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.