English
Let f: α → β' → γ, g: β → β', f' : β → α → δ, g' : δ → γ satisfy h_right_anticomm: ∀ a b, f a (g b) = g' (f' b a). Then image₂ f s (t.image g) = (image₂ f' t s).image g'.
Русский
Пусть 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'.
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha,\\forall t:\\ Finset\\,\\beta,\\forall g:\\beta\\to\\gamma,\\forall f' : \\beta\\to\\alpha\\to\\delta,\\forall g' : \\delta\\to\\gamma,\\ (\\forall a,b, f a (g b) = g' (f' b a)) \\Rightarrow image_2 f s (image_2 t g) = image_2 f' t s . image g' $$$
Lean4
/-- Symmetric statement to `Finset.image_image₂_right_anticomm`. -/
theorem image_image₂_antidistrib_right {g : γ → δ} {f' : β → α' → δ} {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') :=
coe_injective <| by
push_cast
exact image_image2_antidistrib_right h_antidistrib
