English
Symmetric statement to image_image2_right_comm: if g(f(a,b)) = f'(a, g'(b)) then image2 f s t image g = image2 f' s (t.image g').
Русский
Симметричное распределение вправо: если g(f(a,b)) = f'(a, g'(b)), то образ изображения совпадает после применения g к правой части.
LaTeX
$$$\\forall a b,\\ g(f(a,b)) = f'(a, g'(b)) \\Rightarrow \\operatorname{image}_2 f s t = \\operatorname{image}_2 f' s (\\operatorname{image} g' t)$$$
Lean4
/-- Symmetric statement to `Set.image_image2_right_comm`. -/
theorem image_image2_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
(h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (image2 f s t).image g = image2 f' s (t.image g') :=
(image_image2_distrib h_distrib).trans <| by rw [image_id']
