Lists from functions #
Theorems and lemmas for dealing with list.of_fn, which converts a function on fin n to a list
of length n.
Main Definitions #
The main definitions pertain to lists generated using of_fn
list.length_of_fn, which tells us the length of such a listlist.nth_of_fn, which tells us the nth element of such a listlist.array_eq_of_fn, which interprets the list form of an array as such a list.
@[simp]
The length of a list converted from a function is the size of the domain.
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
The nth element of a list
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 : α → β) :
list.map g (list.of_fn f) = list.of_fn (g ∘ f)
Arrays converted to lists are the same as of_fn on the indexing function of the array.
@[simp]
of_fn on an empty domain is the empty list.
@[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.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)
@[simp]
theorem
list.of_fn_const
{α : Type u}
(n : ℕ)
(c : α) :
list.of_fn (λ (i : fin n), c) = list.repeat c n