getElem_pmap — Mathlib

English

Let p and f be as above. For a vector v of length n and index i with i < n, the i-th element of v.pmap f hp is f(v[i]) applied to a proof that p holds for the i-th element.

Русский

Пусть p и f заданы как выше. Для вектора v длины n и индекса i с i < n, i-й элемент v.pmap f hp равен f(v[i]) с доказательством p для i-го элемента.

LaTeX

$$$\forall p:\alpha\to\mathrm{Prop},\ f:(a:\alpha)\to p(a)\to\beta,\ v:\mathrm{Vector}\,\alpha\,n,\ hp:\forall x\in v.toList, p\,x,\ {i:\mathbb{N}}\ (hi:\ i

Lean4

@[simp]
theorem getElem_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) {i : ℕ}
    (hi : i < n) : (v.pmap f hp)[i] = f v[i] (hp _ (by simp [getElem_def, List.getElem_mem])) := by
  simp only [getElem_def, toList_pmap, List.getElem_pmap]

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