Theorems · Definition · combinatorics

Fin.succAboveCases

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

Define a function on Fin (n + 1) from a value on i : Fin (n + 1) and values on each Fin.succAbove i j, j : Fin n. This version is elaborated as eliminator and works for propositions, see also Fin.insertNth for a version without an @[elab_as_elim] attribute.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

9 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext