mapAccumr_map — Mathlib

English

Composition of plain map operations satisfies the usual functorial law: mapping f₁ after mapping f₂ equals mapping the composition f₁ ∘ f₂ over the vector.

Русский

Сопоставление двух функций через map удовлетворяет обычному закону образования произвольного отображения: отображать через f₁ после f₂ эквивалентно отображать через композицию f₁ ∘ f₂.

LaTeX

$$$\operatorname{map} f_1 (\operatorname{map} f_2\ xs) = \operatorname{map} (\lambda x. f_1 (f_2\ x))\ xs$$$

Lean4

@[simp]
theorem mapAccumr_map {s : σ₁} (f₂ : α → β) :
    (mapAccumr f₁ (map f₂ xs) s) = (mapAccumr (fun x s => f₁ (f₂ x) s) xs s) := by
  induction xs using Vector.revInductionOn generalizing s <;> simp_all

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