English
The equivalence consEquiv gives an explicit bijection between a pair consisting of the first element and the tail and the whole sequence.
Русский
Эквивалентность consEquiv задаёт явный биекция между парой (первый элемент, хвост) и полной последовательностью.
LaTeX
$$$\\mathrm{consEquiv} \\;: \\alpha_0 \\times (\\\\forall i, \\\\alpha(\\\\mathrm{succ}\\, i)) \\simeq (\\\\forall i, \\\\alpha 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 first element of the tuple.
This is `Fin.cons` as an `Equiv`. -/
@[simps]
def consEquiv (α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i)) ≃ ∀ i, α i
where
toFun f := cons f.1 f.2
invFun f := (f 0, tail f)
left_inv f := by simp
right_inv f := by simp
