map₂_map_right — Mathlib

English

For vectors xs and ys of the same length, applying map₂ with f1 to xs and the image of ys under f2 equals applying map₂ with the composed function to xs and ys.

Русский

При векторах xs и ys одинаковой длины применение map₂ с f1 к xs и к образу ys через f2 эквивалентно применению map₂ с композиционной функцией к xs и ys.

LaTeX

$$$\operatorname{map}_2 f_1\, xs\,(\operatorname{map} f_2\, ys)=\operatorname{map}_2(\lambda x,y, f_1\, x\,(f_2\, y))\, xs\, ys$$$

Lean4

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

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