Theorems · Definition · combinatorics

Fin.insertNthEquiv

{n : ℕ} →
  (α : Fin (n + 1) → Type u) → (p : Fin (n + 1)) → α p × ((i : Fin n) → α (p.succAbove i)) ≃ ((i : Fin (n + 1)) → α i)

Equivalence between tuples of length n + 1 and pairs of an element and a tuple of length n given by separating out the p-th element of the tuple. This is Fin.insertNth as an Equiv.

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

14 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound