English
Append a tuple of length m to a tuple of length n to obtain a tuple of length m+n. This is the non-dependent version of Fin.addCases.
Русский
Соединение кортежа длины m с кортежем длины n даёт кортеж длины m+n. Это независимая от зависимостей версия Fin.addCases.
LaTeX
$$$\\mathrm{append}: (\\mathrm{Fin}\;m \\to \\alpha) \\to (\\mathrm{Fin}\\;n \\to \\alpha) \\to (\\mathrm{Fin}(m+n) \\to \\alpha)$, тождественно равенству: $\\mathrm{append}(a,b) = \\mathrm{Fin.addCases}(a,b)$.$$
Lean4
/-- Append a tuple of length `m` to a tuple of length `n` to get a tuple of length `m + n`.
This is a non-dependent version of `Fin.add_cases`. -/
def append (a : Fin m → α) (b : Fin n → α) : Fin (m + n) → α :=
@Fin.addCases _ _ (fun _ => α) a b
