English
Let f: α → β' → γ, g: β → β', f': α → β → δ, and g': δ → γ with h_right_comm: f a (g b) = g' (f' a b) for all a,b. Then image₂ f s (t.image g) equals (image₂ f' s t).image g'.
Русский
Пусть f: α → β' → γ, g: β → β', f': α → β → δ, g': δ → γ и h_right_comm: ∀ a,b, f a (g b) = g' (f' a b). Тогда image₂ f s (t.image g) = (image₂ f' s t).image g'.
LaTeX
$$$\\forall s:\\ Finset\\,\\alpha\\,\\forall t:\\ Finset\\,\\beta\\,\\forall f:\\alpha\\to\\beta'\\to\\gamma\\,\\forall g:\\beta\\to\\beta'\\,\\forall f':\\alpha\\to\\beta\\to\\delta\\,\\forall g':\\delta\\to\\gamma,\\ (\\forall a,b, f a (g b) = g' (f' a b))\\Rightarrow image_2 f\\, s\\ (t.image g) = (image_2 f'\\, s\\, t).image g' $$$
Lean4
/-- Symmetric statement to `Finset.image_image₂_distrib_right`. -/
theorem image_image₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
(h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) : image₂ f s (t.image g) = (image₂ f' s t).image g' :=
(image_image₂_distrib_right fun a b => (h_right_comm a b).symm).symm
