Theorems · Theorem · combinatorics

Fin.consCases_cons

∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {motive : ((i : Fin n.succ) → α i) → Sort v}
  (cons : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → motive (Fin.cons x₀ x)) (x₀ : α 0) (x : (i : Fin n) → α i.succ),
  Fin.consCases cons (Fin.cons x₀ x) = cons x₀ x

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

0 results in Mathlib

Foundations

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