Theorems · Theorem · combinatorics

List.Vector.mapAccumr_map

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {n : ℕ} (xs : List.Vector α n) (f₁ : β → σ₁ → σ₁ × γ)
  {s : σ₁} (f₂ : α → β),
  List.Vector.mapAccumr f₁ (List.Vector.map f₂ xs) s = List.Vector.mapAccumr (fun x s => f₁ (f₂ x) s) xs s

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext