English
Let f, g, and g' interact with a, b in such a way that applying g to the result of combining a and b via f is the same as combining b with the image of a under g' via a modified operation f'. Then mapping g over the result of map₂ is the same as applying map₂ with f' to b and a.map g'.
Русский
Пусть существуют такие отображения f, g, g', и элементы a, b типа Option, что применение g к результату сочетания a и b через f совпадает с объединением b и образа a через g', и тогда применение map к результату map₂ совпадает с применением map₂ с f' к b и a.map g'.
LaTeX
$$$\\forall \\alpha, \\beta, \\gamma, \\delta, \\alpha'\\, (f: \\alpha \\to \\beta \\to \\gamma)\\, (a: \\mathrm{Option}\\, \\alpha)\\, (b: \\mathrm{Option}\\, \\beta)\\, (f': \\beta \\to \\alpha' \\to \\delta)\\, (g: \\gamma \\to \\delta)\\, (g': \\alpha \\to \\alpha')\\, (h:\\forall a:\\alpha, b:\\beta, g(f(a,b)) = f'(b)(g'(a))) : \\mathrm{map}\\, g (\\mathrm{map\\_₂}\\, f\\, a\\, b) = \\mathrm{map\\_₂}\\, f'\\, b\\, (\\mathrm{map}\\, g'\\, a) $$
Lean4
/-- Symmetric statement to `Option.map_map₂_right_anticomm`. -/
theorem map_map₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {g' : α → α'}
(h_antidistrib : ∀ a b, g (f a b) = f' b (g' a)) : (map₂ f a b).map g = map₂ f' b (a.map g') := by grind
