English
A variant of right-commutativity: if f a (g b) = g' (f' a b) then image2 f s (t image g) = image2 f' s t image g'.
Русский
Вариант правого коммутирования: если f(a, g(b)) = g'(f'(a,b)), то image2 f s (t image g) = image2 f' s t image g'.
LaTeX
$$$\\forall a b, f(a, g(b)) = g'(f'(a,b)) \\Rightarrow \\operatorname{image}_2 f s (t \\mathrm{image} g) = \\operatorname{image}_2 f' s t \\mathrm{image} g'$$$
Lean4
/-- Symmetric statement to `Set.image_image2_distrib_right`. -/
theorem image_image2_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
(h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) : image2 f s (t.image g) = (image2 f' s t).image g' :=
(image_image2_distrib_right fun a b => (h_right_comm a b).symm).symm
