toList_pmap — Mathlib

English

Converting the pmap of a vector to a list yields the pmap of the list of elements.

Русский

Преобразование pmap вектора к списку даёт pmap списка элементов.

LaTeX

$$$\\mathrm{toList}(\\mathrm{pmap}\\ f\\ v\\ hp) = \\mathrm{List}.pmap\\ f\\ v.\\mathrm{toList}\\ hp$$$

Lean4

@[simp]
theorem toList_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).toList = v.toList.pmap f hp := by cases v; rfl

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