English
Let g: γ → δ, f' : β' → α' → δ, g₁: β → β', g₂: α → α' satisfy h_antidistrib: g (f a b) = f' (g₁ b) (g₂ a) for all a,b. Then (image₂ f s t).image g = image₂ f' (t.image g₁) (s.image g₂).
Русский
Пусть g: γ → δ, f' : β' → α' → δ, g₁ : β → β', g₂ : α → α' удовлетворяют h_antidistrib: g (f a b) = f' (g₁ b) (g₂ a). Тогда (image₂ f s t).image g = image₂ f' (t.image g₁) (s.image g₂).
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha,\\forall t:\\ Finset\\,\\beta,\\forall g:\\gamma\\to\\delta,\\forall f':\\beta'\\to\\alpha'\\to\\delta,\\forall g_1:\\beta\\to\\beta',\\forall g_2:\\alpha\\to\\alpha',\\ (\\forall a,b, g (f a b) = f' (g_1 b) (g_2 a)) \\Rightarrow (image_2 f s t).image g = image_2 f' (t.image g_1) (s.image g_2) $$$
Lean4
theorem image_image₂_antidistrib {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'}
(h_antidistrib : ∀ a b, g (f a b) = f' (g₁ b) (g₂ a)) :
(image₂ f s t).image g = image₂ f' (t.image g₁) (s.image g₂) :=
by
rw [image₂_swap f]
exact image_image₂_distrib fun _ _ => h_antidistrib _ _
