map_map₂_distrib_left — Mathlib

English

A symmetric version of the previous distributive law: mapping g after map₂ f a b equals map₂ f' (a.map g') b when h_distrib holds.

Русский

Симметричная версия распределительного закона: отображение g после map₂ f a b равно map₂ f' (a.map g') b при условии h_distrib.

LaTeX

$$$ \forall a b,\; (\forall a' b', g (f a' b') = f' (g' a') b') \Rightarrow \mathrm{map}\ g (\mathrm{map}_2 f a b) = \mathrm{map}_2 f' (a.map g') b $$$

Lean4

/-- Symmetric statement to `Option.map₂_map_left_comm`. -/
theorem map_map₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'} (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (map₂ f a b).map g = map₂ f' (a.map g') b := by grind

Похожие утверждения