English
Let g: γ → δ, f' : β → α' → δ, g₁ : β → β', g₂ : α → α' satisfy h_antidistrib: ∀ a b, g (f a b) = f' b (g' a). Then (image₂ f s t).image g = image₂ f' t (s.image g').
Русский
Пусть g : γ → δ, f' : β → α' → δ, g₁ : β → β', g₂ : α → α' удовлетворяют h_antidistrib: ∀ a b, g (f a b) = f' b (g' a). Тогда (image₂ f s t).image g = image₂ f' t (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' : \\alpha\\to\\alpha',\\ (\\forall a,b, g (f a b) = f' b (g' a)) \\Rightarrow (image_2 f s t).image g = image_2 f' t (s.image g') $$$
Lean4
/-- Symmetric statement to `Finset.image_image₂_antidistrib_left`. -/
theorem image₂_image_left_anticomm {f : α' → β → γ} {g : α → α'} {f' : β → α → δ} {g' : δ → γ}
(h_left_anticomm : ∀ a b, f (g a) b = g' (f' b a)) : image₂ f (s.image g) t = (image₂ f' t s).image g' :=
(image_image₂_antidistrib_left fun a b => (h_left_anticomm b a).symm).symm
