English
There is an equivalence between words and pairs, given by a forward map and an inverse map rcons.
Русский
Существует эквивалентность между словами и парами, заданная прямым отображением и обратным — rcons.
LaTeX
$$$\\mathrm{equivPair} : \\mathrm{Word}\\, M \\;\\simeq\\; \\mathrm{Pair}\\, M\\, i$ for each i, with toFun w = (equivPairAux\\; i\\; w).val and invFun = \\mathrm{rcons}$$$
Lean4
/-- The equivalence between words and pairs. Given a word, it decomposes it as a pair by removing
the first letter if it comes from `M i`. Given a pair, it prepends the head to the tail. -/
def equivPair (i) : Word M ≃ Pair M i where
toFun w := (equivPairAux i w).val
invFun := rcons
left_inv w := (equivPairAux i w).property
right_inv _ := rcons_inj (equivPairAux i _).property
