Theorems · Theorem · combinatorics

List.Vector.getElem_pmap

∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) (v : List.Vector α n)
  (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n), (List.Vector.pmap f v hp)[i] = f v[i] ⋯

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext