traverse — Mathlib

English

Apply an applicative function to each component of a vector, producing an applicative result vector.

Русский

Применить аппликативную функцию к каждому компоненту вектора, получив вектор с результатами внутри апликатива.

LaTeX

$$$\\text{traverse} : (\\alpha \\to F\\beta) \\to Vector\\alpha\\ n \\to F\\left( Vector\\beta\\ n \\right)$$$

Lean4

/-- Apply an applicative function to each component of a vector. -/
protected def traverse {α β : Type u} (f : α → F β) : Vector α n → F (Vector β n)
  | ⟨v, Hv⟩ => cast (by rw [Hv]) <| traverseAux f v

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