map₂_comm — Mathlib

English

If f is commutative in its first two arguments, i.e. f a1 a2 = f a2 a1 for all a1,a2, then map₂ f xs ys = map₂ f ys xs for vectors xs, ys of the same length.

Русский

Если функция f симметрична по первым двум аргументам, то map₂ f xs ys = map₂ f ys xs для векторов одинаковой длины.

LaTeX

$$$$ \operatorname{map}_2 f\; xs\; ys = \operatorname{map}_2 f\; ys\; xs \quad \text{if } \forall a_1,a_2, f a_1 a_2 = f a_2 a_1 $$$$

Lean4

theorem map₂_comm (f : α → α → β) (comm : ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁) : map₂ f xs ys = map₂ f ys xs := by
  induction xs, ys using Vector.inductionOn₂ <;> simp_all

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