vecAlt1 — Mathlib

English

vecAlt1 selects every odd-indexed element of a vector of even length.

Русский

vecAlt1 выбирает каждый нечётный элемент из вектора чётной длины.

LaTeX

$$$\\text{vecAlt1}(hm,v)(k) = v(k+k+1)$$$

Lean4

/-- `vecAlt1 v` gives a vector with half the length of `v`, with
only alternate elements (odd-numbered). -/
def vecAlt1 (hm : m = n + n) (v : Fin m → α) (k : Fin n) : α :=
  v ⟨(k : ℕ) + k + 1, hm.symm ▸ Nat.add_succ_lt_add k.2 k.2⟩

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