map₂_swap — Mathlib

English

map₂ m f g equals map₂ (λ a b, m b a) g f; equivalently, swapping the arguments in m and the factors yields the same as swapping.

Русский

map₂ m f g равно map₂ (λ a b, m b a) g f; т.е. при перестановке аргументов и факторов получаем то же самое.

LaTeX

$$$ map_2 m f g = map_2 (\lambda a b, m b a) g f $$$

Lean4

theorem map₂_swap (m : α → β → γ) (f : Filter α) (g : Filter β) : map₂ m f g = map₂ (fun a b => m b a) g f :=
  by
  rw [← map_prod_eq_map₂, prod_comm, map_map, ← map_prod_eq_map₂, Function.comp_def]
  simp

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