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

@[simp]
theorem List.length_ofFn_go {α : Type u} {n : } (f : Fin nα) (i : ) (j : ) (h : i + j = n) :
(List.ofFn.go f i j h).length = i
@[simp]
theorem List.length_ofFn {α : Type u} {n : } (f : Fin nα) :
(List.ofFn f).length = n

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

theorem List.getElem_ofFn_go {α : Type u} {n : } (f : Fin nα) (i : ) (j : ) (h : i + j = n) (k : ) (hk : k < (List.ofFn.go f i j h).length) :
(List.ofFn.go f i j h)[k] = f j + k,
theorem List.get_ofFn_go {α : Type u} {n : } (f : Fin nα) (i : ) (j : ) (h : i + j = n) (k : ) (hk : k < (List.ofFn.go f i j h).length) :
(List.ofFn.go f i j h).get k, hk = f j + k,
@[simp]
theorem List.getElem_ofFn {α : Type u} {n : } (f : Fin nα) (i : ) (h : i < (List.ofFn f).length) :
(List.ofFn f)[i] = f i,
theorem List.get_ofFn {α : Type u} {n : } (f : Fin nα) (i : Fin (List.ofFn f).length) :
(List.ofFn f).get i = f (Fin.cast i)
@[simp]
theorem List.getElem?_ofFn {α : Type u} {n : } (f : Fin nα) (i : ) :

The nth element of a list

theorem List.get?_ofFn {α : Type u} {n : } (f : Fin nα) (i : ) :
(List.ofFn f).get? i = List.ofFnNthVal f 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.ofFn f).nthLe i = f i
@[simp, deprecated List.get_ofFn]
theorem List.nthLe_ofFn' {α : Type u} {n : } (f : Fin nα) {i : } (h : i < (List.ofFn f).length) :
(List.ofFn f).nthLe i h = f i,
@[simp]
theorem List.map_ofFn {α : Type u} {β : Type u_1} {n : } (f : Fin nα) (g : αβ) :
theorem List.ofFn_congr {α : Type u} {m : } {n : } (h : m = n) (f : Fin mα) :
List.ofFn f = List.ofFn fun (i : Fin n) => f (Fin.cast 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 n.succα) :
List.ofFn f = f 0 :: List.ofFn fun (i : Fin n) => f i.succ
theorem List.ofFn_succ' {α : Type u} {n : } (f : Fin n.succα) :
List.ofFn f = (List.ofFn fun (i : Fin n) => f i.castSucc).concat (f (Fin.last n))
@[simp]
theorem List.ofFn_eq_nil_iff {α : Type u} {n : } {f : Fin nα} :
List.ofFn f = [] n = 0
theorem List.last_ofFn {α : Type u} {n : } (f : Fin nα) (h : List.ofFn f []) (hn : optParam (n - 1 < n) ) :
(List.ofFn f).getLast h = f n - 1, hn
theorem List.last_ofFn_succ {α : Type u} {n : } (f : Fin n.succα) (h : optParam (List.ofFn f []) ) :
(List.ofFn f).getLast h = f (Fin.last n)
theorem List.ofFn_add {α : Type u} {m : } {n : } (f : Fin (m + n)α) :
List.ofFn f = (List.ofFn fun (i : Fin m) => f (Fin.castAdd n i)) ++ List.ofFn fun (j : Fin n) => f (Fin.natAdd m j)

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.ofFn f = (List.ofFn fun (i : Fin m) => List.ofFn fun (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.ofFn_mul' {α : Type u} {m : } {n : } (f : Fin (m * n)α) :
List.ofFn f = (List.ofFn fun (i : Fin n) => List.ofFn fun (j : Fin m) => f m * i + j, ).join

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

@[simp]
theorem List.ofFn_get {α : Type u} (l : List α) :
List.ofFn l.get = l
@[simp]
theorem List.ofFn_getElem {α : Type u} (l : List α) :
(List.ofFn fun (i : Fin l.length) => l[i]) = l
@[simp]
theorem List.ofFn_getElem_eq_map {α : Type u} {β : Type u_1} (l : List α) (f : αβ) :
(List.ofFn fun (i : Fin l.length) => f l[i]) = List.map f l
@[deprecated List.ofFn_getElem_eq_map]
theorem List.ofFn_get_eq_map {α : Type u} {β : Type u_1} (l : List α) (f : αβ) :
(List.ofFn fun (x : Fin l.length) => f (l.get x)) = List.map f l
@[deprecated List.ofFn_get]
theorem List.ofFn_nthLe {α : Type u} (l : List α) :
(List.ofFn fun (i : Fin l.length) => l.nthLe i ) = l
theorem List.mem_ofFn {α : Type u} {n : } (f : Fin nα) (a : α) :
@[simp]
theorem List.forall_mem_ofFn_iff {α : Type u} {n : } {f : Fin nα} {P : αProp} :
(iList.ofFn f, P i) ∀ (j : Fin n), P (f j)
@[simp]
theorem List.ofFn_const {α : Type u} (n : ) (c : α) :
(List.ofFn fun (x : Fin n) => c) = List.replicate n 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α} :
List.Pairwise R (List.ofFn f) ∀ ⦃i j : Fin n⦄, i < jR (f i) (f j)
@[simp]
theorem List.equivSigmaTuple_symm_apply {α : Type u} (f : (n : ) × (Fin nα)) :
List.equivSigmaTuple.symm f = List.ofFn f.snd
@[simp]
theorem List.equivSigmaTuple_apply_fst {α : Type u} (l : List α) :
(List.equivSigmaTuple l).fst = l.length
@[simp]
theorem List.equivSigmaTuple_apply_snd {α : Type u} (l : List α) :
∀ (a : Fin l.length), (List.equivSigmaTuple l).snd a = l.get a
def List.equivSigmaTuple {α : Type u} :
List α (n : ) × (Fin nα)

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

Equations
  • List.equivSigmaTuple = { toFun := fun (l : List α) => l.length, l.get, invFun := fun (f : (n : ) × (Fin nα)) => List.ofFn f.snd, left_inv := , right_inv := }
Instances For
    def List.ofFnRec {α : Type u} {C : List αSort u_1} (h : (n : ) → (f : Fin nα) → C (List.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.

    Equations
    Instances For
      @[simp]
      theorem List.ofFnRec_ofFn {α : Type u} {C : List αSort u_1} (h : (n : ) → (f : Fin nα) → C (List.ofFn 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.ofFn f)
      theorem List.forall_iff_forall_tuple {α : Type u} {P : List αProp} :
      (∀ (l : List α), P l) ∀ (n : ) (f : Fin nα), P (List.ofFn f)
      theorem List.ofFn_inj' {α : Type u} {m : } {n : } {f : Fin mα} {g : Fin nα} :
      List.ofFn f = List.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 : } :

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

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