English
If g(f a b) = f'(a, g' b) for all a,b, then map₂ f a b mapped by g equals map₂ f' a (map g' b).
Русский
Если для всех a,b выполняется g(f a b) = f'(a, g' b), то map₂ f a b, применяя g, равняется map₂ f' a (map g' b).
LaTeX
$$$\\forall {\\,a:\\,\\alpha}\\, {b:\\,\\beta}\\, {g : \\gamma \\to \\delta}\\, {f' : \\alpha \\to \\beta' \\to \\delta}\\, {g' : \\beta \\to \\beta'},\\; (\\forall a b, g (f a b) = f' a (g' b)) \\\\Rightarrow \\; \\operatorname{Option.map} g (\\operatorname{Option.map}_2 f a b) = \\operatorname{Option.map}_2 f' a (\\operatorname{Option.map} g' b)$$$$
Lean4
/-- Symmetric statement to `Option.map_map₂_right_comm`. -/
theorem map_map₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
(h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (map₂ f a b).map g = map₂ f' a (b.map g') := by grind
