mathlib documentation

data.list.of_fn

Lists from functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

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

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 : array n α) :

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 f = 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 α) :
list.of_fn f = 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 f = (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 α} :
theorem list.last_of_fn {α : Type u} {n : } (f : fin n α) (h : list.of_fn f 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 : list.of_fn f list.nil := _) :
theorem list.of_fn_add {α : Type u} {m n : } (f : fin (m + n) α) :
list.of_fn f = 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.

@[simp]
theorem list.of_fn_fin_append {α : Type u} {m n : } (a : fin m α) (b : fin n α) :
theorem list.of_fn_mul {α : Type u} {m n : } (f : fin (m * n) α) :
list.of_fn f = (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 f = (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 : α) :
@[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.replicate n c
@[simp]
theorem list.of_fn_fin_repeat {α : Type u} {m : } (a : fin m α) (n : ) :
@[simp]
theorem list.pairwise_of_fn {α : Type u} {R : α α Prop} {n : } {f : fin n α} :
list.pairwise R (list.of_fn f) ⦃i j : fin n⦄, i < j R (f i) (f j)
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) :
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 α) :
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 α} :
list.of_fn f = list.of_fn g m, f⟩ = n, g⟩

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

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 α} :

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