mathlib documentation

data.list.of_fn

theorem list.length_of_fn_aux {α : Type u} {n : } (f : fin n → α) (m : ) (h : m n) (l : list α) :

@[simp]
theorem list.length_of_fn {α : Type u} {n : } (f : fin n → α) :

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 : ) :

theorem list.nth_le_of_fn {α : Type u} {n : } (f : fin n → α) (i : fin n) :
(list.of_fn f).nth_le i _ = 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 : α → β) :

theorem list.array_eq_of_fn {α : Type u} {n : } (a : array n α) :

@[simp]
theorem list.of_fn_zero {α : Type u} (f : fin 0 → α) :

@[simp]
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.of_fn_nth_le {α : Type u} (l : list α) :
list.of_fn (λ (i : fin l.length), l.nth_le i _) = l

theorem list.mem_of_fn {α : Type u} {n : } (f : fin n → α) (a : α) :

@[simp]
theorem list.forall_mem_of_fn_iff {α : Type u} {n : } {f : fin n → α} {P : α → Prop} :
(∀ (i : α), i list.of_fn fP i) ∀ (j : fin n), P (f j)

@[simp]
theorem list.of_fn_const {α : Type u} (n : ) (c : α) :
list.of_fn (λ (i : fin n), c) = list.repeat c n