English
If h_assoc is a compatibility condition between m, n, m', n', then map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h).
Русский
Если существует совместимость h_assoc между m, n, m', n', то map₂ m (map₂ n f g) h равно map₂ m' f (map₂ n' g h).
LaTeX
$$$ (\forall a b c, m (n a b) c = m' a (n' b c)) \to map_2 m (map_2 n f g) h = map_2 m' f (map_2 n' g h) $$$
Lean4
theorem map₂_assoc {m : δ → γ → ε} {n : α → β → δ} {m' : α → ε' → ε} {n' : β → γ → ε'} {h : Filter γ}
(h_assoc : ∀ a b c, m (n a b) c = m' a (n' b c)) : map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h) :=
by
rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right, ← map_prod_eq_map₂, ←
map_prod_eq_map₂, ← prod_assoc, map_map]
simp only [h_assoc, Function.comp_def, Equiv.prodAssoc_apply]
