shiftFun — Mathlib

English

Define shiftFun, which sends a function on Fin n to a function on Fin (n+1) by placing a zero in the head and shifting the rest.

Русский

Определим shiftFun, который переводит функцию на Fin n в функцию на Fin (n+1), помещая в начало ноль и сдвигая остальные значения.

LaTeX

$${n} \to {X} \to (Fin n \to X) \to (Fin (n+1) \to X), \; shiftFun(f)(i) = 0 if i=0, \; shiftFun(f)(i.succ) = f(i)$$

Lean4

/-- When `[Zero X]`, the shift of a map `f : Fin n → X`
is a map `Fin (n + 1) → X` which sends `0` to `0` and `i.succ` to `f i`. -/
def shiftFun {n : ℕ} {X : Type*} [Zero X] (f : Fin n → X) (i : Fin (n + 1)) : X :=
  Matrix.vecCons 0 f i

Похожие утверждения