map₂_swap — Mathlib

English

Swapping the two arguments in map₂ yields the same result up to swapping the order of arguments inside the function.

Русский

Смена порядка аргументов в map₂ эквивалентна тому же выражению с перестановкой аргументов внутри функции.

LaTeX

$$$ \mathrm{map}_2\ f\ a\ b = \mathrm{map}_2\ (\lambda a b. f b a)\ b\ a $$$

Lean4

theorem map₂_swap (f : α → β → γ) (a : Option α) (b : Option β) : map₂ f a b = map₂ (fun a b => f b a) b a := by grind

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