English
Given a position j in Fin(n+1), a binary operation op on α, a sequence g: Fin(n+1) → α, and an index k in Fin n, define the contracted sequence by inserting op between the j-th and (j+1)-st entries and shifting the later entries; in other words, the k-th entry is g(k) when k is before j, is op(g(k before), g(k after)) when k equals j, and is g(k+1) otherwise.
Русский
Дано положение j в Fin(n+1), двоичную операцию op на α, последовательность g: Fin(n+1) → α и индекс k в Fin n. Определим сжатую последовательность путём вставки операции между j-й и (j+1)-й элементами и сдвига элементов после. Элемент с индексом k равен g(k) до позиции j, равен op(g(до), g(после)) когда k = j, и равен g(k+1) если k после.
LaTeX
$$$\\text{contractNth}(j,\\ op, g)(k) = \\begin{cases} g(\\text{castSucc }k), & (k:\\mathbb{N}) < j, \\\\ op(g(\\text{castSucc }k), g(k.succ)), & (k:\\mathbb{N}) = j, \\\\ g(k.succ), & \\text{otherwise}. \\end{cases}$$$
Lean4
/-- Sends `(g₀, ..., gₙ)` to `(g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ)`. -/
def contractNth (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) : α :=
if (k : ℕ) < j then g (Fin.castSucc k) else if (k : ℕ) = j then op (g (Fin.castSucc k)) (g k.succ) else g k.succ
