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