English
Symmetric statement to antidistrib_left/antidistrib_right: map maps to reversed order in two-argument map₂ with swapped arguments.
Русский
Симметричное утверждение к антираспределению слева/справа: map переносит отображение в обратном порядке при смене аргументов.
LaTeX
$$$\\forall {g : \\gamma \\to \\delta} {f' : \\beta' \\to \\alpha' \\to \\delta} {g_1 : \\beta \\to \\beta'} {g_2 : \\alpha \\to \\alpha'} (h_antidistrib : \\forall a b, g (f a b) = f' (g_1 b) (g_2 a)) : \\operatorname{Option.map} g (\\operatorname{Option.map}_2 f a b) = \\operatorname{Option.map}_2 f' (\\operatorname{Option.map} g_1 b) (\\operatorname{Option.map} g_2 a)$$$$
Lean4
/-- Symmetric statement to `Option.map_map₂_distrib_right`. -/
theorem map_map₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
(h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) : map₂ f a (b.map g) = (map₂ f' a b).map g' := by grind
