English
remapLeft f k transforms inputs on the left part using f and shifts the right part, giving Fin2 (m+k) → Fin2 (n+k).
Русский
remapLeft f k преобразует левую часть входа с помощью f и сдвигает правую часть, получая отображение Fin2(m+k) → Fin2(n+k).
LaTeX
$$$\text{remapLeft} : (f : Fin2\ m \to Fin2\ n) \to \forall k,\ Fin2(m+k) \to Fin2(n+k)$, заданное по кейсам: $0 \mapsto f0$, $k+1,\mathrm{fz} \mapsto \mathrm{fz}$, $k+1, i \mapsto \mathrm{fs}(\text{remapLeft } f\ k\ i)$.$$
Lean4
/-- `remapLeft f k : Fin2 (m + k) → Fin2 (n + k)` applies the function
`f : Fin2 m → Fin2 n` to inputs less than `m`, and leaves the right part
on the right (that is, `remapLeft f k (m + i) = n + i`). -/
def remapLeft {m n} (f : Fin2 m → Fin2 n) : ∀ k, Fin2 (m + k) → Fin2 (n + k)
| 0, i => f i
| _k + 1, @fz _ => fz
| _k + 1, @fs _ i => fs (remapLeft f _ i)
