Theorems · Theorem · combinatorics

List.Vector.mapAccumr_redundant_pair

∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} {n : ℕ} {s : σ} {xs : List.Vector α n} (f : α → σ × σ → (σ × σ) × β),
  (∀ (x : α) (s : σ), (f x (s, s)).1.1 = (f x (s, s)).1.2) →
    (List.Vector.mapAccumr f xs (s, s)).2 =
      (List.Vector.mapAccumr (fun x s => ((f x (s, s)).1.1, (f x (s, s)).2)) xs s).2

If f takes a pair of states, but always returns the same value for both elements of the pair, then we can simplify to just a single element of state.

Defined in

Mathlib.Data.Vector.MapLemmas

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound