Theorems · Definition · combinatorics

Fin.consCases

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

Recurse on an n+1-tuple by splitting it into a single element and an n-tuple.

Defined in: Mathlib.Data.Fin.Tuple.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 34 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Fin.consstatement and proof · cited by 190
Fin.tailproof · cited by 74

Cited by4

Results whose statement or proof uses this declaration.

ConnectedComponents.exists_fun_isClopen_of_infiniteproof · cited by 1
Set.iUnion_fin_add_one_eq_iUnion_succproof · cited by 1
Fin.consCases_consstatement · cited by 0
Fin.forall_fin_succ_piproof · cited by 0