English
If g is a function on γ and f and g' are compatible with a right-distributive law, then (image₂ f s t).image g = image₂ f s (t.image g').
Русский
Если g действует справа и совместим с f, g', тогда образ двойного образа равен образу справа.
LaTeX
$$$\forall a,b,\ g (f a b) = f' a (g' b) \Rightarrow (\mathrm{image}_2 f\ s\ t).\mathrm{image}\ g = \mathrm{image}_2 f' s (t.\mathrm{image}\ g')$$$
Lean4
/-- Symmetric statement to `Finset.image_image₂_right_comm`. -/
theorem image_image₂_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
(h_distrib : ∀ a b, g (f a b) = f' a (g' b)) : (image₂ f s t).image g = image₂ f' s (t.image g') :=
coe_injective <| by
push_cast
exact image_image2_distrib_right h_distrib