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