mapAccumr₂_flip — Mathlib

English

Same as above; this lemma states that applying the flip to f yields the corresponding relation for mapAccumr₂.

Русский

То же, что и выше; лемма утверждает, что применение операции flip к f даёт соответствующее соотношение для mapAccumr₂.

LaTeX

$$$$ \operatorname{mapAccumr_2} f\; xs\; ys\; s = \operatorname{mapAccumr_2} (\mathrm{flip}\, f)\; ys\; xs\; s $$$$

Lean4

theorem mapAccumr₂_flip (f : α → β → σ → σ × γ) : mapAccumr₂ f xs ys s = mapAccumr₂ (flip f) ys xs s := by
  induction xs, ys using Vector.inductionOn₂ <;> simp_all [flip]

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