# Documentation

Mathlib.Data.List.OfFn

# Lists from functions #

Theorems and lemmas for dealing with List.ofFn, which converts a function on Fin n to a list of length n.

## Main Statements #

The main statements pertain to lists generated using List.ofFn

• List.length_ofFn, which tells us the length of such a list
• List.get?_ofFn, which tells us the nth element of such a list
• List.equivSigmaTuple, which is an Equiv between lists and the functions that generate them via List.ofFn.
@[simp]
theorem List.length_ofFn {α : Type u} {n : } (f : Fin nα) :
= n

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

@[simp]
theorem List.get_ofFn {α : Type u} {n : } (f : Fin nα) (i : Fin ()) :
List.get () i = f (Fin.cast (_ : = n) i)
@[simp]
theorem List.get?_ofFn {α : Type u} {n : } (f : Fin nα) (i : ) :
List.get? () i =

The nth element of a list

@[deprecated List.get_ofFn]
theorem List.nthLe_ofFn {α : Type u} {n : } (f : Fin nα) (i : Fin n) :
List.nthLe () i (_ : i < ) = f i
@[simp, deprecated List.get_ofFn]
theorem List.nthLe_ofFn' {α : Type u} {n : } (f : Fin nα) {i : } (h : i < ) :
List.nthLe () i h = f { val := i, isLt := (_ : i < n) }
@[simp]
theorem List.map_ofFn {α : Type u} {β : Type u_1} {n : } (f : Fin nα) (g : αβ) :
List.map g () = List.ofFn (g f)
theorem List.ofFn_congr {α : Type u} {m : } {n : } (h : m = n) (f : Fin mα) :
= List.ofFn fun i => f (Fin.cast (_ : n = m) i)
@[simp]
theorem List.ofFn_zero {α : Type u} (f : Fin 0α) :
= []

ofFn on an empty domain is the empty list.

@[simp]
theorem List.ofFn_succ {α : Type u} {n : } (f : Fin ()α) :
= f 0 :: List.ofFn fun i => f ()
theorem List.ofFn_succ' {α : Type u} {n : } (f : Fin ()α) :
= List.concat (List.ofFn fun i => f ()) (f ())
@[simp]
theorem List.ofFn_eq_nil_iff {α : Type u} {n : } {f : Fin nα} :
= [] n = 0
theorem List.last_ofFn {α : Type u} {n : } (f : Fin nα) (h : []) (hn : optParam (n - 1 < n) (_ : Nat.pred (Nat.sub n 0) < Nat.sub n 0)) :
= f { val := n - 1, isLt := hn }
theorem List.last_ofFn_succ {α : Type u} {n : } (f : Fin ()α) (h : optParam ( []) (_ : ¬ = [])) :
= f ()
theorem List.ofFn_add {α : Type u} {m : } {n : } (f : Fin (m + n)α) :
= (List.ofFn fun i => f ()) ++ List.ofFn fun j => f ()

Note this matches the convention of List.ofFn_succ', putting the Fin m elements first.

@[simp]
theorem List.ofFn_fin_append {α : Type u} {m : } {n : } (a : Fin mα) (b : Fin nα) :
theorem List.ofFn_mul {α : Type u} {m : } {n : } (f : Fin (m * n)α) :
= List.join (List.ofFn fun i => List.ofFn fun j => f { val := i * n + j, isLt := (_ : i * n + j < m * n) })

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

theorem List.ofFn_mul' {α : Type u} {m : } {n : } (f : Fin (m * n)α) :
= List.join (List.ofFn fun i => List.ofFn fun j => f { val := m * i + j, isLt := (_ : m * i + j < m * n) })

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

theorem List.ofFn_get {α : Type u} (l : List α) :
= l
@[deprecated List.ofFn_get]
theorem List.ofFn_nthLe {α : Type u} (l : List α) :
(List.ofFn fun i => List.nthLe l i (_ : i < )) = l
theorem List.mem_ofFn {α : Type u} {n : } (f : Fin nα) (a : α) :
a a
@[simp]
theorem List.forall_mem_ofFn_iff {α : Type u} {n : } {f : Fin nα} {P : αProp} :
((i : α) → i P i) (j : Fin n) → P (f j)
@[simp]
theorem List.ofFn_const {α : Type u} (n : ) (c : α) :
(List.ofFn fun x => c) =
@[simp]
theorem List.ofFn_fin_repeat {α : Type u} {m : } (a : Fin mα) (n : ) :
@[simp]
theorem List.pairwise_ofFn {α : Type u} {R : ααProp} {n : } {f : Fin nα} :
i j : Fin n⦄ → i < jR (f i) (f j)
@[simp]
theorem List.equivSigmaTuple_apply_fst {α : Type u} (l : List α) :
(List.equivSigmaTuple l).fst =
@[simp]
theorem List.equivSigmaTuple_apply_snd {α : Type u} (l : List α) :
∀ (a : Fin ()), Sigma.snd (fun n => Fin nα) (List.equivSigmaTuple l) a = List.get l a
@[simp]
theorem List.equivSigmaTuple_symm_apply {α : Type u} (f : (n : ) × (Fin nα)) :
List.equivSigmaTuple.symm f = List.ofFn f.snd
def List.equivSigmaTuple {α : Type u} :
List α (n : ) × (Fin nα)

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

Instances For
def List.ofFnRec {α : Type u} {C : List αSort u_1} (h : (n : ) → (f : Fin nα) → C ()) (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.ofFnRec.

Instances For
@[simp]
theorem List.ofFnRec_ofFn {α : Type u} {C : List αSort u_1} (h : (n : ) → (f : Fin nα) → C ()) {n : } (f : Fin nα) :
= h n f
theorem List.exists_iff_exists_tuple {α : Type u} {P : List αProp} :
(l, P l) n f, P ()
theorem List.forall_iff_forall_tuple {α : Type u} {P : List αProp} :
((l : List α) → P l) (n : ) → (f : Fin nα) → P ()
theorem List.ofFn_inj' {α : Type u} {m : } {n : } {f : Fin mα} {g : Fin nα} :
{ fst := m, snd := f } = { fst := n, snd := g }

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

theorem List.ofFn_injective {α : Type u} {n : } :

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

@[simp]
theorem List.ofFn_inj {α : Type u} {n : } {f : Fin nα} {g : Fin nα} :
f = g

A special case of List.ofFn_inj for when the two functions are indexed by defeq n.