ofRepeat — Mathlib

English

There is a projection map ofRepeat that, given a type α and an index i in Fin2 n, returns the i-th element of a repeat n α vector.

Русский

Существует отображение ofRepeat, которое, имея α и индекс i в Fin2 n, возвращает i-ю компоненту повторяющегося вектора длины n.

LaTeX

$$$\\mathrm{ofRepeat} {\\alpha} {i} : {\\text{repeat}}\,n\,\\alpha\\,i \\to \\alpha.$$$

Lean4

/-- projection for a repeat vector -/
def ofRepeat {α : Sort _} : ∀ {n i}, «repeat» n α i → α
  | _, Fin2.fz => fun (a : α) => a
  | _, Fin2.fs i => @ofRepeat _ _ i

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