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

theorem List.get_ofFn {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (ofFn f).length) : (ofFn f).get i = f (Fin.cast ⋯ i)

theorem List.ofFn_comp' {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β) : (ofFn fun (i : Fin n) => g (f i)) = map g (ofFn f)

Useful if rw [← map_ofFn] complains that g ∘ f is not the same as fun i => g (f i).

theorem List.ofFn_congr {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α) : ofFn f = ofFn fun (i : Fin n) => f (Fin.cast ⋯ i)

theorem List.ofFn_succ' {α : Type u} {n : ℕ} (f : Fin n.succ → α) : ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).concat (f (Fin.last n))

@[simp]

theorem List.ofFn_fin_append {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α) : ofFn (Fin.append a b) = ofFn a ++ ofFn b

theorem List.ofFn_mul {α : Type u} {m n : ℕ} (f : Fin (m * n) → α) : ofFn f = (ofFn fun (i : Fin m) => ofFn fun (j : Fin n) => f ⟨↑i * n + ↑j, ⋯⟩).flatten

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) → α) : ofFn f = (ofFn fun (i : Fin n) => ofFn fun (j : Fin m) => f ⟨m * ↑i + ↑j, ⋯⟩).flatten

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

@[simp]

theorem List.ofFn_get {α : Type u} (l : List α) : ofFn l.get = l

@[simp]

theorem List.ofFn_getElem_eq_map {α : Type u} {β : Type u_1} (l : List α) (f : α → β) : (ofFn fun (i : Fin l.length) => f l[↑i]) = map f l

theorem List.mem_ofFn' {α : Type u} {n : ℕ} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f

theorem List.forall_mem_ofFn_iff {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)

@[simp]

theorem List.ofFn_const {α : Type u} (n : ℕ) (c : α) : (ofFn fun (x : Fin n) => c) = replicate n c

@[simp]

theorem List.ofFn_fin_repeat {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ) : ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

@[simp]

theorem List.pairwise_ofFn {α : Type u} {R : α → α → Prop} {n : ℕ} {f : Fin n → α} : Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

@[deprecated List.pairwise_ofFn (since := "2025-10-11")]

theorem List.sorted_ofFn_iff {α : Type u} {R : α → α → Prop} {n : ℕ} {f : Fin n → α} : Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Alias of List.pairwise_ofFn.

theorem List.getLast_ofFn_succ {α : Type u} {n : ℕ} (f : Fin n.succ → α) : (ofFn f).getLast ⋯ = f (Fin.last n)

theorem List.ofFn_cons {α : Type u} {n : ℕ} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f

theorem List.find?_ofFn_eq_some {α : Type u} {n : ℕ} {f : Fin n → α} {p : α → Bool} {b : α} : find? p (ofFn f) = some b ↔ p b = true ∧ ∃ (i : Fin n), f i = b ∧ ∀ j < i, ¬p (f j) = true

theorem List.find?_ofFn_eq_some_of_injective {α : Type u} {n : ℕ} {f : Fin n → α} {p : α → Bool} {i : Fin n} (h : Function.Injective f) : find? p (ofFn f) = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬p (f j) = true

def List.equivSigmaTuple {α : Type u} : List α ≃ (n : ℕ) × (Fin n → α)

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

@[simp]

theorem List.equivSigmaTuple_symm_apply {α : Type u} (f : (n : ℕ) × (Fin n → α)) : equivSigmaTuple.symm f = ofFn f.snd

@[simp]

theorem List.equivSigmaTuple_apply_snd {α : Type u} (l : List α) (a✝ : Fin l.length) : (equivSigmaTuple l).snd a✝ = l.get a✝

@[simp]

theorem List.equivSigmaTuple_apply_fst {α : Type u} (l : List α) : (equivSigmaTuple l).fst = l.length

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

@[simp]

theorem List.ofFnRec_ofFn {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)) {n : ℕ} (f : Fin n → α) : ofFnRec h (ofFn f) = h n f

theorem List.exists_iff_exists_tuple {α : Type u} {P : List α → Prop} : (∃ (l : List α), P l) ↔ ∃ (n : ℕ) (f : Fin n → α), P (ofFn f)

theorem List.forall_iff_forall_tuple {α : Type u} {P : List α → Prop} : (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (ofFn f)

theorem List.ofFn_inj' {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α} : ofFn f = ofFn g ↔ ⟨m, f⟩ = ⟨n, 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 : ℕ} : Function.Injective ofFn

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

@[simp]

theorem List.ofFn_inj {α : Type u} {n : ℕ} {f g : Fin n → α} : ofFn f = ofFn g ↔ f = g

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