English
Let f, g, and a transformation g' interact so that f (g a) b equals g' (f' b a) for all a, b. Then map₂ with f applied to (a.map g) and b equals the mapped result of f' with b and a, followed by g'.
Русский
Пусть существует соответствие между f, g и преобразованием g' так, что f (g a) b = g' (f' b a) для всех a, b. Тогда map₂, применяемый к (a.map g) и b, равен отображению g' над результатом map₂ с f' и аргументами b и a.
LaTeX
$$$\\forall {\\alpha, \\beta, \\gamma, \\delta} {f: \\alpha' \\to \\beta \\to \\gamma} {g: \\alpha \\to \\alpha'} {f': \\beta \\to \\alpha \\to \\delta} {g': \\delta \\to \\gamma} (h_{left}: \\forall a b, f (g a) b = g' (f' b a)) : \\mathrm{map\\_₂}\\, f\\ (\\mathrm{map}\\ g\\ a) \\ b = \\mathrm{map}\\ g' (\\mathrm{map\\_₂}\\, f'\\, b\\ a) $$
Lean4
/-- Symmetric statement to `Option.map_map₂_antidistrib_left`. -/
theorem map₂_map_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
(h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) : map₂ f (a.map g) b = (map₂ f' b a).map g' := by grind
