English
Symmetric statement to map_map₂_antidistrib_left: (map₂ f a b).map g = map₂ f' (b.map g') a given a left-antidistributive law.
Русский
Симметричное утверждение к map_map₂_antidistrib_left: (map₂ f a b).map g = map₂ f' (b.map g') a при левом антираспределении.
LaTeX
$$$\\forall {\\alpha \\beta \\gamma \\delta} {f : \\alpha \\to \\beta \\to \\gamma} {a : \\mathrm{Option}\\, \\alpha} {b : \\mathrm{Option}\\, \\beta} {\\beta' : Type*} {g : \\gamma \\to \\delta} {f' : \\beta' \\to \\alpha \\to \\delta} {g' : \\beta \\to \\beta'},\\; (\\forall (a : \\alpha) (b : \\beta), g (f a b) = f' (g' b) a) \\\\Rightarrow \\; \\operatorname{Option.map} g (\\operatorname{Option.map}_2 f a b) = \\operatorname{Option.map}_2 f' (\\operatorname{Option.map} g' b) a$$$$
Lean4
/-- Symmetric statement to `Option.map₂_map_left_anticomm`. -/
theorem map_map₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
(h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) : (map₂ f a b).map g = map₂ f' (b.map g') a := by grind
