English
If a distribution relation property holds: n (m a b) = m' b (n' a) for all a,b, then composing maps yields an equality: map n (map₂ m f g) = map₂ m' g (map n' f).
Русский
Если выполняется распределительная связь: n(m(a,b)) = m'(b, n'(a)) для всех a,b, то применение map n к результату map₂ m f g равно map₂ m' g (map n' f).
LaTeX
$$$\big(\forall a,b,\ n(m\ a\ b) = m'\ (b)\ (n'\ a)\big) \Rightarrow \mathrm{Eq}(\mathrm{map}\ n (\mathrm{map}_2 m\ f\ g)) (\mathrm{map}_2 m'\ g (\mathrm{map}\ n' f))$$$
Lean4
/-- Symmetric statement to `Filter.map_map₂_right_anticomm`. -/
theorem map_map₂_antidistrib_right {n : γ → δ} {m' : β → α' → δ} {n' : α → α'}
(h_antidistrib : ∀ a b, n (m a b) = m' b (n' a)) : (map₂ m f g).map n = map₂ m' g (f.map n') :=
map_map₂_antidistrib h_antidistrib
