English
If n distributes over m via n1 and n2: ∀ a b, n (m a b) = m' (n1 a) (n2 b), then applying map n to map₂ m f g equals map₂ m' applied to f.map n1 and g.map n2.
Русский
Если n распределяет через m: ∀ a b, n (m a b) = m' (n1 a) (n2 b), тогда $\mathrm{map}\, (\mathrm{map}_2 m f g) = \mathrm{map}_2 m' (f.map n_1) (g.map n_2)$.
LaTeX
$$$\mathrm{map}\, (\mathrm{map}_2 m\, f\, g) = \mathrm{map}_2 m' (f\ map n_1) (g\ map n_2)$
\text{with } n (m a b) = m' (n_1 a) (n_2 b)$$
Lean4
theorem map_map₂_distrib {n : γ → δ} {m' : α' → β' → δ} {n₁ : α → α'} {n₂ : β → β'}
(h_distrib : ∀ a b, n (m a b) = m' (n₁ a) (n₂ b)) : (map₂ m f g).map n = map₂ m' (f.map n₁) (g.map n₂) := by
simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]
