English
Suppose we have f, g, f', g' with a left-commuting law: for all a,b,c, f(a, g(b,c)) = g'(b, f'(a,c)). Then image2 f (s, image2 g t u) = image2 g' t (image2 f' s u).
Русский
Пусть существуют отображения f, g, f', g', удовлетворяющие условию левого коммутирования: для всех a,b,c выполняется f(a, g(b,c)) = g'(b, f'(a,c)). Тогда image2 f (s, image2 g t u) = image2 g' t (image2 f' s u).
LaTeX
$$$\\forall a,b,c:\\ f(a, g(b,c)) = g'(b, f'(a,c)) \\Rightarrow \\operatorname{image}_2 f (s, \\operatorname{image}_2 g t u) = \\operatorname{image}_2 g' t (\\operatorname{image}_2 f' s u)$$$
Lean4
theorem image2_assoc {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'}
(h_assoc : ∀ a b c, f (g a b) c = f' a (g' b c)) : image2 f (image2 g s t) u = image2 f' s (image2 g' t u) :=
eq_of_forall_subset_iff fun _ ↦ by simp only [image2_subset_iff, forall_mem_image2, h_assoc]
