mapAccumr₂_snoc — Mathlib

English

mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = let q := f x y s; let r := mapAccumr₂ f xs ys q.1 in (r.1, r.2.snoc q.2).

Русский

mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = пусть q := f x y s; пусть r := mapAccumr₂ f xs ys q.1; в конце (r.1, r.2.snoc q.2).

LaTeX

$$$\text{mapAccumr₂ } f (xs.snoc x) (ys.snoc y) s =\ \ let q := f x y s \\n let r := mapAccumr₂ f xs ys q.1 \\n \ (r.1, r.2.snoc q.2)$$$

Lean4

@[simp]
theorem mapAccumr₂_snoc (f : α → β → σ → σ × φ) (x : α) (y : β) :
    mapAccumr₂ f (xs.snoc x) (ys.snoc y) s =
      let q := f x y s
      let r := mapAccumr₂ f xs ys q.1
      (r.1, r.2.snoc q.2) :=
  by induction xs, ys using Vector.inductionOn₂ <;> simp_all

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