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