English
Let p be a predicate on elements and f a dependent map that assigns to each a with p(a) a value in β. If v is a vector of length n+1 whose elements all satisfy p, then the head of the mapped vector (obtained by applying f to each element with the corresponding proof) is exactly f applied to the head of v with the appropriate proof of p for that head.
Русский
Пусть p — предикат на элементы, а f — зависимое отображение, которое каждому элементу a с p(a) ставит в соответствие значение в β. Пусть v — вектор длины n+1 над α, все элементы которого удовлетворяют p. Тогда голова векторa, полученного отображением pmap f hp, равна f(head(v)) с соответствующим доказательством p(head(v)).
LaTeX
$$$\forall p:\alpha\to\mathrm{Prop},\ f:(a:\alpha)\to p(a)\to\beta,\ v:\mathrm{Vector}\,\alpha\,(n+1),\ hp:\forall x\in v.toList, p\,x\;\to\ \mathrm{head}(\mathrm{pmap}\ f\ hp) = f(\mathrm{head}(v))\ hp_{\text{head}}$$$
Lean4
@[simp]
theorem head_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) :
(v.pmap f hp).head =
f v.head (hp _ <| by rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]; exact .inl rfl) :=
by
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
simp_rw [h, pmap_cons, head_cons]
