Theorems · Theorem · combinatorics

List.Vector.map_mapAccumr

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

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext