Theorems · Theorem · combinatorics

Fin.update_cons_zero

∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (x : α 0) (p : (i : Fin n) → α i.succ) (z : α 0),
  Function.update (Fin.cons x p) 0 z = Fin.cons z p

Adding an element at the beginning of a tuple and then updating it amounts to adding it directly.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

4 results in Mathlib

Foundations

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