Theorems · Definition · combinatorics

List.Vector.pmap

{α : Type u_1} →
  {β : Type u_2} →
    {n : ℕ} → {p : α → Prop} → ((a : α) → p a → β) → (v : List.Vector α n) → (∀ x ∈ v.toList, p x) → List.Vector β n

Map a vector under a partial function.

Defined in

Mathlib.Data.Vector.Defs

Cited by

10 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext