scilib documentation

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.

source
theorem set.range_list_map {α : Type u_1} {β : Type u_2} (f : α → β) :
set.range (list.map f) = {l : list β | ∀ (x : β), x ∈ l → x ∈ set.range f}
source
theorem set.range_list_map_coe {α : Type u_1} (s : set α) :
set.range (list.map coe) = {l : list α | ∀ (x : α), x ∈ l → x ∈ s}
source
@[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}
source
theorem set.range_list_nth {α : Type u_1} (l : list α) :
set.range l.nth = has_insert.insert option.none (option.some '' {x : α | x ∈ l})
source
@[simp]
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}
source
@[simp]
theorem set.range_list_inth {α : Type u_1} [inhabited α] (l : list α) :
set.range l.inth = has_insert.insert inhabited.default {x : α | x ∈ l}
source
@[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 β) (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