English
Let g: γ → δ, f : α → β → γ, f' : β' → α' → δ, g₁ : β → β', g₂ : α → α' satisfy h_antidistrib: ∀ a b, g (f a b) = f' b (g' a). Then image₂ f s t on g equals image₂ f' t (s.image g').
Русский
Пусть g: γ → δ, f: α → β → γ, f' : β' → α' → δ, g₁, g₂ удовлетворяют сопряжённому правилу: ∀ a,b, g (f a b) = f' b (g' a). Тогда image₂ f s t на g равно image₂ f' t (s.image g').
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha,\\forall t:\\ Finset\\,\\beta,\\ (\\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_right`. -/
theorem image_image₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
(h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) : image₂ f s (t.image g) = (image₂ f' t s).image g' :=
(image_image₂_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm
