Theorems · Theorem · combinatorics

Fin.snoc_init_self

∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i), Fin.snoc (Fin.init q) (q (Fin.last n)) = q

Concatenating the first element of a tuple with its tail gives back the original tuple

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

7 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Quot.sound