mapAccumr₂_mapAccumr_right — Mathlib

English

A composed accumulation identity: applying mapAccumr₂ to xs, ys and then mapAccumr on the right yields the same as a nested composition.

Русский

Утверждение о равенстве при компоновке mapAccumr₂ и mapAccumr: получаем одинаковый результат.

LaTeX

$$$\forall xs\!:\mathrm{List.Vector}\;\alpha\;n,\; \forall ys:\mathrm{List.Vector}\;\beta\;n,\; \text{...} = \text{...}$$$

Lean4

@[simp]
theorem mapAccumr₂_mapAccumr_right (f₁ : α → γ → σ₁ → σ₁ × ζ) (f₂ : β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ xs (mapAccumr f₂ ys s₂).snd s₁) =
      let m :=
        (mapAccumr₂
          (fun x y s =>
            let r₂ := f₂ y s.snd
            let r₁ := f₁ x r₂.snd s.fst
            ((r₁.fst, r₂.fst), r₁.snd))
          xs ys (s₁, s₂))
      (m.fst.fst, m.snd) :=
  by induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

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