English
A left-commutation identity for image₂: if ∀ a b c, f a (g b c) = g' b (f' a c), then image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u).
Русский
Левая коммутативность для image₂: если ∀ a b c выполняется f a (g b c) = g' b (f' a c), то image₂ f s (image₂ g t u) = image₂ g' t (image₂ f' s u).
LaTeX
$$$\forall a,b,c,\ f\ a\ (g\ b\ c) = g'\ b\ (f'\ a\ c) \Rightarrow \mathrm{image}_2\ f\ s (\mathrm{image}_2\ g\ t\ u) = \mathrm{image}_2\ g'\ t (\mathrm{image}_2\ f'\ s\ u)$$$
Lean4
theorem image_image₂_distrib {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'}
(h_distrib : ∀ a b, g (f a b) = f' (g₁ a) (g₂ b)) : (image₂ f s t).image g = image₂ f' (s.image g₁) (t.image g₂) :=
coe_injective <| by
push_cast
exact image_image2_distrib h_distrib
