map_map₂ — Mathlib

English

A standard compatibility: mapping after map₂ equals mapping composed function over xs, ys.

Русский

Совместимость: отображение после map₂ эквивалентно отображению после композиции над x и y.

LaTeX

$$$\forall xs,\;\forall ys,\;\forall f_1,f_2,\; \mathrm{map}\,f_1\; (\mathrm{map\_2}\; f_2\; xs\; ys) = \mathrm{map\_2}\; (\lambda x,y. f_1( f_2 x y))\; xs\; ys$$$

Lean4

@[simp]
theorem map_map₂ (f₁ : γ → ζ) (f₂ : α → β → γ) : map f₁ (map₂ f₂ xs ys) = map₂ (fun x y => f₁ <| f₂ x y) xs ys := by
  induction xs, ys using Vector.revInductionOn₂ <;> simp_all

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