mathlib3 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

source
theorem list.length_of_fn_aux {α : Type u} {n : ℕ} (f : fin n → α) (m : ℕ) (h : m ≤ n) (l : list α) :
(list.of_fn_aux f m h l).length = l.length + m
source
@[simp]
theorem list.length_of_fn {α : Type u} {n : ℕ} (f : fin n → α) :
(list.of_fn f).length = n

The length of a list converted from a function is the size of the domain.

source
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
source
@[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

source
theorem list.nth_le_of_fn {α : Type u} {n : ℕ} (f : fin n → α) (i : fin n) :
(list.of_fn f).nth_le ↑i _ = f i
source
@[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, _⟩
source
@[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)
source
theorem list.array_eq_of_fn {α : Type u} {n : ℕ} (a : array n α) :
a.to_list = list.of_fn a.read

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

source
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))
source
@[simp]
theorem list.of_fn_zero {α : Type u} (f : fin 0 → α) :
list.of_fn f = list.nil

of_fn on an empty domain is the empty list.

source
@[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)
source
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))
source
@[simp]
theorem list.of_fn_eq_nil_iff {α : Type u} {n : ℕ} {f : fin n → α} :
list.of_fn f = list.nil ↔ n = 0
source
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⟩
source
theorem list.last_of_fn_succ {α : Type u} {n : ℕ} (f : fin n.succ → α) (h : list.of_fn f ≠ list.nil := _) :
(list.of_fn f).last h = f (fin.last n)
source
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.

source
@[simp]
theorem list.of_fn_fin_append {α : Type u} {m n : ℕ} (a : fin m → α) (b : fin n → α) :
list.of_fn (fin.append a b) = list.of_fn a ++ list.of_fn b
source
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.

source
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.

source
theorem list.of_fn_nth_le {α : Type u} (l : list α) :
list.of_fn (λ (i : fin l.length), l.nth_le ↑i _) = l
source
theorem list.mem_of_fn {α : Type u} {n : ℕ} (f : fin n → α) (a : α) :
a ∈ list.of_fn f ↔ a ∈ set.range f
source
@[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)
source
@[simp]
theorem list.of_fn_const {α : Type u} (n : ℕ) (c : α) :
list.of_fn (λ (i : fin n), c) = list.replicate n c
source
@[simp]
theorem list.of_fn_fin_repeat {α : Type u} {m : ℕ} (a : fin m → α) (n : ℕ) :
list.of_fn (fin.repeat n a) = (list.replicate n (list.of_fn a)).join
source
@[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)
source
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
source
@[simp]
theorem list.equiv_sigma_tuple_apply_snd {α : Type u} (l : list α) (i : fin l.length) :
(⇑list.equiv_sigma_tuple l).snd i = l.nth_le ↑i _
source
@[simp]
theorem list.equiv_sigma_tuple_apply_fst {α : Type u} (l : list α) :
(⇑list.equiv_sigma_tuple l).fst = l.length
source
@[simp]
theorem list.equiv_sigma_tuple_symm_apply {α : Type u} (f : Σ (n : ℕ), fin n → α) :
⇑(list.equiv_sigma_tuple.symm) f = list.of_fn f.snd
source
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
source
@[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_rec h (list.of_fn f) = h n f
source
theorem list.exists_iff_exists_tuple {α : Type u} {P : list α → Prop} :
(∃ (l : list α), P l) ↔ ∃ (n : ℕ) (f : fin n → α), P (list.of_fn f)
source
theorem list.forall_iff_forall_tuple {α : Type u} {P : list α → Prop} :
(∀ (l : list α), P l) ↔ ∀ (n : ℕ) (f : fin n → α), P (list.of_fn f)
source
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.

source
theorem list.of_fn_injective {α : Type u} {n : ℕ} :
function.injective list.of_fn

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

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

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