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 : α → β) : Set.range (List.map f) = {l | ∀ (x : β), x ∈ l → x ∈ Set.range f}

theorem Set.range_list_map_coe {α : Type u_1} (s : Set α) : Set.range (List.map Subtype.val) = {l | ∀ (x : α), x ∈ l → x ∈ s}

@[simp]

theorem Set.range_list_nthLe {α : Type u_1} (l : List α) : (Set.range fun k => List.nthLe l ↑k (_ : ↑k < List.length l)) = {x | x ∈ l}

theorem Set.range_list_get? {α : Type u_1} (l : List α) : Set.range (List.get? l) = 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} [Inhabited α] (l : List α) : Set.range (List.getI l) = insert default {x | x ∈ l}

instance List.canLift {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (List α) (List β) (List.map c) fun l => (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

• @List.canLift = @List.canLift.proof_1