data.list.of_fn

# 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 Statements #

The main statements pertain to lists generated using of_fn

• list.length_of_fn, which tells us the length of such a list
• list.nth_of_fn, which tells us the nth element of such a list
• list.array_eq_of_fn, which interprets the list form of an array as such a list.
• list.equiv_sigma_tuple, which is an equiv between lists and the functions that generate them via list.of_fn.
theorem list.length_of_fn_aux {α : Type u} {n : } (f : fin n → α) (m : ) (h : m n) (l : list α) :
m h l).length = l.length + m
@[simp]
theorem list.length_of_fn {α : Type u} {n : } (f : fin n → α) :

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 = (i + m)) m h l).nth i =
@[simp]
theorem list.nth_of_fn {α : Type u} {n : } (f : fin n → α) (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 : α → β) :
theorem list.array_eq_of_fn {α : Type u} {n : } (a : α) :

Arrays converted to lists are the same as of_fn on the indexing function of the array.

theorem list.of_fn_congr {α : Type u} {m n : } (h : m = n) (f : fin m → α) :
= list.of_fn (λ (i : fin n), f ((fin.cast _) i))
@[simp]
theorem list.of_fn_zero {α : Type u} (f : fin 0 → α) :

of_fn on an empty domain is the empty list.

@[simp]
theorem list.of_fn_succ {α : Type u} {n : } (f : fin n.succ → α) :
= f 0 :: list.of_fn (λ (i : fin n), f i.succ)
theorem list.of_fn_succ' {α : Type u} {n : } (f : fin n.succ → α) :
= (list.of_fn (λ (i : fin n), f (fin.cast_succ i))).concat (f (fin.last n))
@[simp]
theorem list.of_fn_eq_nil_iff {α : Type u} {n : } {f : fin n → α} :
n = 0
theorem list.last_of_fn {α : Type u} {n : } (f : fin n → α) (h : list.nil) (hn : n - 1 < n := _) :
(list.of_fn f).last h = f n - 1, hn⟩
theorem list.last_of_fn_succ {α : Type u} {n : } (f : fin n.succ → α) (h : := _) :
theorem list.of_fn_add {α : Type u} {m n : } (f : fin (m + n) → α) :
= list.of_fn (λ (i : fin m), f ((fin.cast_add n) i)) ++ list.of_fn (λ (j : fin n), f ((fin.nat_add m) j))

Note this matches the convention of list.of_fn_succ', putting the fin m elements first.

theorem list.of_fn_mul {α : Type u} {m n : } (f : fin (m * n) → α) :
= (list.of_fn (λ (i : fin m), list.of_fn (λ (j : fin n), f i * n + j, _⟩))).join

This breaks a list of m*n items into m groups each containing n elements.

theorem list.of_fn_mul' {α : Type u} {m n : } (f : fin (m * n) → α) :
= (list.of_fn (λ (i : fin n), list.of_fn (λ (j : fin m), f m * i + j, _⟩))).join

This breaks a list of m*n items into n groups each containing m elements.

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 : α) :
a a
@[simp]
theorem list.forall_mem_of_fn_iff {α : Type u} {n : } {f : fin n → α} {P : α → Prop} :
(∀ (i : α), i 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) = n
def list.equiv_sigma_tuple {α : Type u} :
list α Σ (n : ), fin n → α

Lists are equivalent to the sigma type of tuples of a given length.

Equations
@[simp]
theorem list.equiv_sigma_tuple_apply_snd {α : Type u} (l : list α) (i : fin l.length) :
= l.nth_le i _
@[simp]
theorem list.equiv_sigma_tuple_apply_fst {α : Type u} (l : list α) :
@[simp]
theorem list.equiv_sigma_tuple_symm_apply {α : Type u} (f : Σ (n : ), fin n → α) :
def list.of_fn_rec {α : Type u} {C : list αSort u_1} (h : Π (n : ) (f : fin n → α), C (list.of_fn f)) (l : list α) :
C l

A recursor for lists that expands a list into a function mapping to its elements.

This can be used with induction l using list.of_fn_rec.

Equations
@[simp]
theorem list.of_fn_rec_of_fn {α : Type u} {C : list αSort u_1} (h : Π (n : ) (f : fin n → α), C (list.of_fn f)) {n : } (f : fin n → α) :
(list.of_fn f) = h n f
theorem list.exists_iff_exists_tuple {α : Type u} {P : list α → Prop} :
(∃ (l : list α), P l) ∃ (n : ) (f : fin n → α), P (list.of_fn f)
theorem list.forall_iff_forall_tuple {α : Type u} {P : list α → Prop} :
(∀ (l : list α), P l) ∀ (n : ) (f : fin n → α), P (list.of_fn f)
theorem list.of_fn_inj' {α : Type u} {m n : } {f : fin m → α} {g : fin n → α} :
m, f⟩ = n, g⟩

fin.sigma_eq_iff_eq_comp_cast may be useful to work with the RHS of this expression.

theorem list.of_fn_injective {α : Type u} {n : } :

Note we can only state this when the two functions are indexed by defeq n.

@[simp]
theorem list.of_fn_inj {α : Type u} {n : } {f g : fin n → α} :
f = g

A special case of list.of_fn_inj' for when the two functions are indexed by defeq n.