@[simp]
theorem
list.nth_of_fn_aux
{α : Type u}
{n : ℕ}
(f : fin n → α)
(i m : ℕ)
(h : m ≤ n)
(l : list α) :
(∀ (i : ℕ), l.nth i = list.of_fn_nth_val f (i + m)) → (list.of_fn_aux f m h l).nth i = list.of_fn_nth_val f i
@[simp]
theorem
list.nth_of_fn
{α : Type u}
{n : ℕ}
(f : fin n → α)
(i : ℕ) :
(list.of_fn f).nth i = list.of_fn_nth_val f i
theorem
list.nth_le_of_fn
{α : Type u}
{n : ℕ}
(f : fin n → α)
(i : fin n) :
(list.of_fn f).nth_le i.val _ = f i
@[simp]
theorem
list.nth_le_of_fn'
{α : Type u}
{n : ℕ}
(f : fin n → α)
{i : ℕ}
(h : i < (list.of_fn f).length) :
(list.of_fn f).nth_le i h = f ⟨i, _⟩
@[simp]
theorem
list.map_of_fn
{α : Type u}
{β : Type u_1}
{n : ℕ}
(f : fin n → α)
(g : α → β) :
list.map g (list.of_fn f) = list.of_fn (g ∘ f)
theorem
list.of_fn_succ
{α : Type u}
{n : ℕ}
(f : fin n.succ → α) :
list.of_fn f = f 0 :: list.of_fn (λ (i : fin n), f i.succ)
theorem
list.mem_of_fn
{α : Type u}
{n : ℕ}
(f : fin n → α)
(a : α) :
a ∈ list.of_fn f ↔ a ∈ set.range f
@[simp]
theorem
list.forall_mem_of_fn_iff
{α : Type u}
{n : ℕ}
{f : fin n → α}
{P : α → Prop} :
(∀ (i : α), i ∈ list.of_fn f → P i) ↔ ∀ (j : fin n), P (f j)