English
Mapping with a predicate-respecting function through pmap is compatible with pmap on the original vector as long as the predicate respects membership in the underlying list.
Русский
Отображение через f₂, сохраняющее свойство p, через pmap совместимо с pmap на исходном векторе, если предикат p учитывает принадлежность элементу базового списка.
LaTeX
$$$\text{map } f_1 (\text{pmap } f_2 xs H) = \text{pmap } (\lambda x hx. f_1 (f_2 x) hx) xs H$$$
Lean4
@[simp]
theorem map_mapAccumr {s : σ₂} (f₁ : β → γ) :
(map f₁ (mapAccumr f₂ xs s).snd) =
(mapAccumr
(fun x s =>
let r := (f₂ x s);
(r.fst, f₁ r.snd))
xs s).snd :=
by induction xs using Vector.revInductionOn generalizing s <;> simp_all
