map_map₂_distrib — Mathlib

English

If g distributes over f via h_distrib, then mapping g over map₂ f a b equals map₂ f' (a.map g₁) (b.map g₂).

Русский

Если g распределяется над f через h_distrib, то отображение g над map₂ f a b равно map₂ f' (a.map g₁) (b.map g₂).

LaTeX

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

Lean4

theorem map_map₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) : (map₂ f a b).map g = map₂ f' (a.map g₁) (b.map g₂) := by grind

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