English
Map a vector under a partial function f : (a) → p a → β, provided a proof hp that every element satisfies p. The result is a vector β n with the given predicate satisfied for each element.
Русский
Отображение вектора частичной функцией f: (a) → p a → β, при условии hp: для каждого элемента выполняется p. Результат — вектор β n, элементы которого удовлетворяют предикату.
LaTeX
$$$\\mathrm{pmap}\\,f\\,\\langle l,h\\rangle\\;:\\; (\\forall x\\in l,\\ p\\ x)\\to\\text{Vector }\\beta n\\ ,\\text{with underlying list }(\\text{List.pmap } f\\, l\\ hp)$$$
Lean4
/-- Map a vector under a partial function. -/
def pmap (f : (a : α) → p a → β) : (v : Vector α n) → (∀ x ∈ v.toList, p x) → Vector β n
| ⟨l, h⟩, hp => ⟨List.pmap f l hp, by simp [h]⟩
