Theorems · Definition · combinatorics

Fin.insertNth

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

Insert an element into a tuple at a given position. For i = 0 see Fin.cons, for i = Fin.last n see Fin.snoc. See also Fin.succAboveCases for a version elaborated as an eliminator.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

95 results in Mathlib

Foundations

Depth 31 from the axioms, rests on 264 definitions · uses propext