English
If two-argument operation m is symmetric to n after swapping the order of its arguments, i.e. m a b = n b a for all a, b, then the induced two-variable maps commute: map₂ m f g = map₂ n g f for any filters f on α and g on β.
Русский
Если двуарный оператор m симметричен к n после перестановки аргументов, то индуцированные отображения равны: map₂ m f g = map₂ n g f для любых фильтров f на α и g на β.
LaTeX
$$$\mathrm{map}_2 m\,f\,g = \mathrm{map}_2 n\,g\,f$
\text{under the assumption } m\,a\,b = n\,b\,a\text{ for all }a,b.$$
Lean4
theorem map₂_comm {n : β → α → γ} (h_comm : ∀ a b, m a b = n b a) : map₂ m f g = map₂ n g f :=
(map₂_swap _ _ _).trans <| by simp_rw [h_comm]
