English
Symmetric statement to the previous one: if m a (n b) = n' (m' b a), then map₂ m f (g.map n) = (map₂ m' g f).map n'.
Русский
Симметричное отношение: если m a (n b) = n' (m' b a), то map₂ m f (g.map n) = (map₂ m' g f).map n'.
LaTeX
$$$\big(\forall a,b,\ m a (n b) = n' (m' b a)\big) \Rightarrow \mathrm{Eq}(\mathrm{map}_2 m f (\mathrm{map} n g)) (\mathrm{map} n' (\mathrm{map}_2 m' g f))$$$
Lean4
/-- Symmetric statement to `Filter.map_map₂_antidistrib_right`. -/
theorem map_map₂_right_anticomm {m : α → β' → γ} {n : β → β'} {m' : β → α → δ} {n' : δ → γ}
(h_right_anticomm : ∀ a b, m a (n b) = n' (m' b a)) : map₂ m f (g.map n) = (map₂ m' g f).map n' :=
(map_map₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm
