Mathlib.Data.Finsupp.Fin

Finsupp.tail definition

(s : Fin (n + 1) →₀ M) : Fin n →₀ M

Full source

/-- `tail` for maps `Fin (n + 1) →₀ M`. See `Fin.tail` for more details. -/
def tail (s : FinFin (n + 1) →₀ M) : FinFin n →₀ M :=
  Finsupp.equivFunOnFinite.symm (Fin.tail s)

Tail of a finitely supported function on `Fin (n + 1)`

Informal description

The function `Finsupp.tail` takes a finitely supported function `s : Fin (n + 1) →₀ M` and returns its tail, which is a finitely supported function `Fin n →₀ M` obtained by removing the first element of `s`. More precisely, for each index `i : Fin n`, the value of the tail at `i` is equal to the value of `s` at `i.succ`.

Finsupp.cons definition

(y : M) (s : Fin n →₀ M) : Fin (n + 1) →₀ M

Full source

/-- `cons` for maps `Fin n →₀ M`. See `Fin.cons` for more details. -/
def cons (y : M) (s : FinFin n →₀ M) : FinFin (n + 1) →₀ M :=
  Finsupp.equivFunOnFinite.symm (Fin.cons y s : Fin (n + 1) → M)

Prepending an element to a finitely supported function on $\mathrm{Fin}\,n$

Informal description

Given an element $y \in M$ and a finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$, the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ is defined as the finitely supported function corresponding to the tuple obtained by prepending $y$ to the tuple represented by $s$. Specifically, $\mathrm{cons}\,y\,s$ maps $0$ to $y$ and $i.\mathrm{succ}$ to $s\,i$ for each $i \colon \mathrm{Fin}\,n$.

Finsupp.tail_apply theorem

: tail t i = t i.succ

Full source

theorem tail_apply : tail t i = t i.succ :=
  rfl

Tail Function Evaluation: $\mathrm{tail}\,t\,i = t\,i.\mathrm{succ}$

Informal description

For any finitely supported function $t \colon \mathrm{Fin}\,(n+1) \to₀ M$ and any index $i \colon \mathrm{Fin}\,n$, the value of the tail function $\mathrm{tail}\,t$ at $i$ is equal to the value of $t$ at the successor index $i.\mathrm{succ}$, i.e., $\mathrm{tail}\,t\,i = t\,i.\mathrm{succ}$.

Finsupp.cons_zero theorem

: cons y s 0 = y

Full source

@[simp]
theorem cons_zero : cons y s 0 = y :=
  rfl

$\mathrm{cons}\,y\,s(0) = y$ for finitely supported functions

Informal description

For any element $y \in M$ and any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$, the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ satisfies $\mathrm{cons}\,y\,s(0) = y$.

Finsupp.cons_succ theorem

: cons y s i.succ = s i

Full source

@[simp]
theorem cons_succ : cons y s i.succ = s i :=
  rfl

Successor Evaluation of Cons Function: $\mathrm{cons}\,y\,s(i.\mathrm{succ}) = s(i)$

Informal description

For any element $y \in M$, any finitely supported function $s \colon \mathrm{Fin}\,n \to M$ with finite support, and any index $i \colon \mathrm{Fin}\,n$, the function $\mathrm{cons}\,y\,s$ evaluated at the successor index $i.\mathrm{succ}$ equals $s$ evaluated at $i$, i.e., $\mathrm{cons}\,y\,s(i.\mathrm{succ}) = s(i)$.

Finsupp.tail_cons theorem

: tail (cons y s) = s

Full source

@[simp]
theorem tail_cons : tail (cons y s) = s :=
  ext fun k => by simp only [tail_apply, cons_succ]

Tail of a Cons Operation on Finitely Supported Functions

Informal description

For any element $y \in M$ and any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$, the tail of the function $\mathrm{cons}\,y\,s$ is equal to $s$. That is, $\mathrm{tail}(\mathrm{cons}\,y\,s) = s$.

Finsupp.tail_update_zero theorem

: tail (update t 0 y) = tail t

Full source

@[simp]
theorem tail_update_zero : tail (update t 0 y) = tail t := by simp [tail]

Tail Preservation Under Zero-Index Update in Finitely Supported Functions

Informal description

For any finitely supported function $t \colon \mathrm{Fin}(n+1) \to M$ and any element $y \in M$, the tail of the updated function obtained by setting the value at index $0$ to $y$ is equal to the tail of the original function $t$. That is, $\mathrm{tail}(t.\mathrm{update}\,0\,y) = \mathrm{tail}(t)$.

Finsupp.tail_update_succ theorem

: tail (update t i.succ y) = update (tail t) i y

Full source

@[simp]
theorem tail_update_succ : tail (update t i.succ y) = update (tail t) i y := by ext; simp [tail]

Tail of Updated Function at Successor Index Equals Updated Tail

Informal description

For any finitely supported function $t \colon \text{Fin} (n+1) \to M$, any index $i \colon \text{Fin} n$, and any value $y \in M$, the tail of the updated function $t$ at $i.\text{succ}$ with value $y$ is equal to the function obtained by updating the tail of $t$ at $i$ with value $y$. In other words, \[ \text{tail}(t.\text{update}\,(i.\text{succ})\,y) = (\text{tail}\,t).\text{update}\,i\,y. \]

Finsupp.cons_tail theorem

: cons (t 0) (tail t) = t

Full source

@[simp]
theorem cons_tail : cons (t 0) (tail t) = t := by
  ext a
  by_cases c_a : a = 0
  · rw [c_a, cons_zero]
  · rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]

Reconstruction of Finitely Supported Function via Cons and Tail: $\mathrm{cons}(t(0), \mathrm{tail}(t)) = t$

Informal description

For any finitely supported function $t \colon \mathrm{Fin}(n+1) \to M$, the function obtained by prepending $t(0)$ to the tail of $t$ is equal to $t$ itself. That is, $\mathrm{cons}(t(0), \mathrm{tail}(t)) = t$.

Finsupp.cons_zero_zero theorem

: cons 0 (0 : Fin n →₀ M) = 0

Full source

@[simp]
theorem cons_zero_zero : cons 0 (0 : FinFin n →₀ M) = 0 := by
  ext a
  by_cases c : a = 0
  · simp [c]
  · rw [← Fin.succ_pred a c, cons_succ]
    simp

Prepending Zero to Zero Function Yields Zero Function

Informal description

For any natural number $n$, the function obtained by prepending $0$ to the zero function $\mathrm{Fin}\,n \to₀ M$ is equal to the zero function $\mathrm{Fin}\,(n+1) \to₀ M$. That is, $\mathrm{cons}\,0\,0 = 0$.

Finsupp.cons_ne_zero_of_left theorem

(h : y ≠ 0) : cons y s ≠ 0

Full source

theorem cons_ne_zero_of_left (h : y ≠ 0) : conscons y s ≠ 0 := by
  contrapose! h with c
  rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply]

Nonzero Prepended Element Yields Nonzero Finitely Supported Function

Informal description

For any element $y \in M$ and any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$, if $y \neq 0$, then the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ is not identically zero.

Finsupp.cons_ne_zero_of_right theorem

(h : s ≠ 0) : cons y s ≠ 0

Full source

theorem cons_ne_zero_of_right (h : s ≠ 0) : conscons y s ≠ 0 := by
  contrapose! h with c
  ext a
  simp [← cons_succ a y s, c]

Nonzero Finitely Supported Function Remains Nonzero After Prepending an Element

Informal description

For any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$ that is not identically zero, and for any element $y \in M$, the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ is also not identically zero.

Finsupp.cons_ne_zero_iff theorem

: cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

Full source

theorem cons_ne_zero_iff : conscons y s ≠ 0cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0 := by
  refine ⟨fun h => ?_, fun h => h.casesOn cons_ne_zero_of_left cons_ne_zero_of_right⟩
  refine imp_iff_not_or.1 fun h' c => h ?_
  rw [h', c, Finsupp.cons_zero_zero]

Nonzero Condition for Prepended Finitely Supported Function: $\mathrm{cons}\,y\,s \neq 0 \leftrightarrow y \neq 0 \lor s \neq 0$

Informal description

For any element $y \in M$ and any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$, the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ is nonzero if and only if either $y \neq 0$ or $s$ is not the zero function.

Finsupp.cons_support theorem

: (s.cons y).support ⊆ insert 0 (s.support.map (Fin.succEmb n))

Full source

lemma cons_support : (s.cons y).support ⊆ insert 0 (s.support.map (Fin.succEmb n)) := by
  intro i hi
  suffices i = 0 ∨ ∃ a, ¬s a = 0 ∧ a.succ = i by simpa
  apply (Fin.eq_zero_or_eq_succ i).imp id (Exists.imp _)
  rintro i rfl
  simpa [Finsupp.mem_support_iff] using hi

Support of Cons Function is Contained in Zero Union Successor of Support

Informal description

For any finitely supported function $s \colon \mathrm{Fin}\,n \to₀ M$ and any element $y \in M$, the support of the function $\mathrm{cons}\,y\,s \colon \mathrm{Fin}\,(n+1) \to₀ M$ is contained in the union of $\{0\}$ with the image of the support of $s$ under the successor embedding $\mathrm{Fin}\,n \to \mathrm{Fin}\,(n+1)$. In other words, $\mathrm{supp}(\mathrm{cons}\,y\,s) \subseteq \{0\} \cup \mathrm{succ}[\mathrm{supp}(s)]$.

Finsupp.cons_right_injective theorem

{n : ℕ} {M : Type*} [Zero M] (y : M) : Injective (Finsupp.cons y : (Fin n →₀ M) → Fin (n + 1) →₀ M)

Full source

lemma cons_right_injective {n : ℕ} {M : Type*} [Zero M] (y : M) :
    Injective (Finsupp.cons y : (FinFin n →₀ M) → FinFin (n + 1) →₀ M) :=
  (equivFunOnFinite.symm.injective.comp ((Fin.cons_right_injective _).comp DFunLike.coe_injective))

Injectivity of Prepending an Element to Finitely Supported Functions on $\mathrm{Fin}\,n$

Informal description

For any natural number $n$, any type $M$ with a zero element, and any element $y \in M$, the function $\mathrm{cons}\,y \colon (\mathrm{Fin}\,n \to₀ M) \to (\mathrm{Fin}\,(n+1) \to₀ M)$ is injective. That is, if $\mathrm{cons}\,y\,s_1 = \mathrm{cons}\,y\,s_2$ for two finitely supported functions $s_1, s_2 \colon \mathrm{Fin}\,n \to₀ M$, then $s_1 = s_2$.