English
Equivalence between a pair of a p-th element and a tail, and the full array, via insertNth and removeNth.
Русский
Эквивалентность между парой: p-й элемент и хвост, и полным массивом через insertNth и removeNth.
LaTeX
$$$$ \text{insertNthEquiv} \;: \ α_{p} \times (\forall i, α_{p.succAbove i}) \\simeq \forall i, α_{i} $$$$
Lean4
/-- 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`. -/
@[simps]
def insertNthEquiv (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) : α p × (∀ i, α (p.succAbove i)) ≃ ∀ i, α i
where
toFun f := insertNth p f.1 f.2
invFun f := (f p, removeNth p f)
left_inv f := by ext <;> simp
right_inv f := by simp
