English
If h_right_comm: ∀a,b,c, m (n a b) c = n' (m' a c) b, then map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g.
Русский
При условии правого переноса: ∀a,b,c, m (n a b) c = n' (m' a c) b выполняется, тогда выполняется равенство: map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g.
LaTeX
$$$\mathrm{map}_2\,m\, (\mathrm{map}_2\,n\,f\,g)\,h = \mathrm{map}_2\,n'\,(\mathrm{map}_2\,m'\,f\,h)\,g$$$
Lean4
theorem map₂_right_comm {m : δ → γ → ε} {n : α → β → δ} {m' : α → γ → δ'} {n' : δ' → β → ε}
(h_right_comm : ∀ a b c, m (n a b) c = n' (m' a c) b) : map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g :=
by
rw [map₂_swap n, map₂_swap n']
exact map₂_assoc fun _ _ _ => h_right_comm _ _ _
