mapAccumr_snoc — Mathlib

English

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

Русский

mapAccumr f (xs.snoc x) s = пусть q := f x s; пусть r := mapAccumr f xs q.1; тогда (r.1, r.2.snoc q.2).

LaTeX

$$$\text{mapAccumr } f (xs.snoc x) s = \text{let } q := f x s; \text{ let } r := \text{mapAccumr } f xs q.1 \text{ in } (r.1, r.2.snoc q.2)$$$

Lean4

@[simp]
theorem mapAccumr_snoc {f : α → σ → σ × β} {s : σ} :
    mapAccumr f (xs.snoc x) s =
      let q := f x s
      let r := mapAccumr f xs q.1
      (r.1, r.2.snoc q.2) :=
  by
  induction xs
  · rfl
  · simp [*]

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