English
If h_left_comm holds: ∀a,b,c, m a (n b c) = n' b (m' a c), then combining maps is commutative in a left-rotation sense: map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h).
Русский
Если выполняется тождество левого переноса: ∀a,b,c, m a (n b c) = n' b (m' a c), тогда сочетания отображений удовлетворяют равенству слева: map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h).
LaTeX
$$$\mathrm{map}_2\,m\,f\bigl(\mathrm{map}_2\,n\,g\,h\bigr) = \mathrm{map}_2\,n'\,g\bigl(\mathrm{map}_2\,m'\,f\,h\bigr)$$$
Lean4
theorem map₂_left_comm {m : α → δ → ε} {n : β → γ → δ} {m' : α → γ → δ'} {n' : β → δ' → ε}
(h_left_comm : ∀ a b c, m a (n b c) = n' b (m' a c)) : map₂ m f (map₂ n g h) = map₂ n' g (map₂ m' f h) :=
by
rw [map₂_swap m', map₂_swap m]
exact map₂_assoc fun _ _ _ => h_left_comm _ _ _
