map₂_flip — Mathlib

English

For any binary operation f : α → β → γ and any vectors xs : Vector α n and ys : Vector β n, map₂ f xs ys equals map₂ (flip f) ys xs. This expresses a symmetry of map₂ under swapping the inputs.

Русский

Для любой бинарной операции f : α → β → γ и любых векторов xs : Vector α n и ys : Vector β n, map₂ f xs ys равно map₂ (flip f) ys xs. Это выражает симметрию map₂ при перестановке входов.

LaTeX

$$$\mathrm{map_2}\ f\ xs\ ys = \mathrm{map_2}\ (\mathrm{flip}\ f)\ ys\ xs$$$

Lean4

theorem map₂_flip (f : α → β → γ) : map₂ f xs ys = map₂ (flip f) ys xs := by
  induction xs, ys using Vector.inductionOn₂ <;> simp_all [flip]

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