Theorems · Definition · combinatorics

Fin.snoc

{n : ℕ} → {α : Fin (n + 1) → Sort u_1} → ((i : Fin n) → α i.castSucc) → α (Fin.last n) → (i : Fin (n + 1)) → α i

Adding an element at the end of an n-tuple, to get an n+1-tuple. The name snoc comes from cons (i.e., adding an element to the left of a tuple) read in reverse order.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

113 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 115 definitions · uses no axioms