English
If g distributes over f in the sense that g(f(a,b)) = f'(g1(a), g2(b)), then applying g after image2 f over s and t equals image2 f' over the images of s and t under g1 and g2 respectively.
Русский
Если g распределяет f по формуле g(f(a,b)) = f'(g1(a), g2(b)), то образ g после image2 f над s,t равен image2 f' над с и t после применения g1, g2.
LaTeX
$$$\\forall a b,\\ g(f(a,b)) = f'(g_1(a), g_2(b)) \\Rightarrow (\\operatorname{image}_2 f\\ s\\ t)\\!\\!\\to\\!\\! \\operatorname{image} g (\\operatorname{image}_2 f s t) = \\operatorname{image}_2 f' (\\operatorname{image} g_1 s) (\\operatorname{image} g_2 t)$$$
Lean4
theorem image_image2_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
(h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) : (image2 f s t).image g = image2 f' (s.image g₁) (t.image g₂) :=
by simp_rw [image_image2, image2_image_left, image2_image_right, h_distrib]
