mapAccumr₂_comm — Mathlib

English

If f is commutative in its first two arguments, then swapping the two input vectors yields the same mapAccumr₂ result: mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s.

Русский

Если f коммутативна по первым двум аргументам, то обмен левых и правых входных векторов не влияет на результат: mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s.

LaTeX

$$$$ \operatorname{mapAccumr_2} f\; xs\; ys\; s = \operatorname{mapAccumr_2} f\; ys\; xs\; s $$$$

Lean4

theorem mapAccumr₂_comm (f : α → α → σ → σ × γ) (comm : ∀ a₁ a₂ s, f a₁ a₂ s = f a₂ a₁ s) :
    mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s := by
  induction xs, ys using Vector.inductionOn₂ generalizing s <;> simp_all

Похожие утверждения