English
If applying g on the right side of a binary operation composed with maps yields a commuted form with f' and g', then map₂ with a on the left and b.map g is equal to the mapped result of f' with b and a, followed by g'.
Русский
Если применение g справа в результате сочетания операций можно привести к формуле, используя f' и g', то равенство распространяется на левую часть map₂: map₂ f (a.map g) b = (map₂ f' b a).map g'.
LaTeX
$$$\\forall {\\alpha, \\beta, \\gamma, \\delta} {f: \\alpha \\to \\beta' \\to \\gamma} {g: \\beta \\to \\beta'} {f': \\beta \\to \\alpha \\to \\delta} {g': \\delta \\to \\gamma} (h_{right}: \\forall a b, f a (g b) = g' (f' b a)) : \\mathrm{map\\_₂}\\, f\\ a (\\mathrm{map}\\ g\\ b) = (\\mathrm{map\\_₂}\\, f'\\, b\\ a).map\\ g' $$
Lean4
/-- Symmetric statement to `Option.map_map₂_antidistrib_right`. -/
theorem map_map₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
(h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) : map₂ f a (b.map g) = (map₂ f' b a).map g' := by grind
