English
Symmetric version of the above: if m (n a) b = n' (m' b a) for all a,b, then map₂ m (f.map n) g = (map₂ m' g f).map n'.
Русский
Косвенная симметрия: если m (n a) b = n' (m' b a) для всех a,b, то map₂ m (f.map n) g = (map₂ m' g f).map n'.
LaTeX
$$$\big(\forall a,b,\ m (n a) b = n' (m' b a)\big) \Rightarrow \mathrm{Eq}(\mathrm{map}_2 m (\mathrm{map} n f) g) (\mathrm{map} n' (\mathrm{map}_2 m' g f))$$$
Lean4
/-- Symmetric statement to `Filter.map_map₂_antidistrib_left`. -/
theorem map₂_map_left_anticomm {m : α' → β → γ} {n : α → α'} {m' : β → α → δ} {n' : δ → γ}
(h_left_anticomm : ∀ a b, m (n a) b = n' (m' b a)) : map₂ m (f.map n) g = (map₂ m' g f).map n' :=
(map_map₂_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm
