English
pmap distributes over cons: mapping with hp over a cons equals cons of mapped head and pmap of the tail.
Русский
pmap распределяет умножение над консом: отображение через f над cons даёт конc из отображённого головы и pmap по хвосту.
LaTeX
$$$\\mathrm{List.Vector}.pmap\\ f\\ (\\mathrm{cons}\\ a\\ v)\\ hp = \\mathrm{cons}\\ (f\\ a\\ hp_1)\\ (\\mathrm{List.Vector}.pmap\\ f\\ v\\ hp_2)$$$
Lean4
@[simp]
theorem pmap_cons {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (hp : ∀ x ∈ (cons a v).toList, p x) :
(cons a v).pmap f hp =
cons
(f a
(by
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
exact hp.1))
(v.pmap f
(by
simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
exact hp.2)) :=
rfl
