English
Symmetric form of image2_left_comm: if f(g(a), b) = g'(f'(a,b)) then image2 f (image g s t) t = (image2 f' s t).image g'.
Русский
Симметричная форма для left_comm: если f(g(a), b) = g'(f'(a,b)), то image2 f (image g s t) t = (image2 f' s t).image g'.
LaTeX
$$$\\forall a b, f(g(a,b)) = g'(f'(a,b)) \\Rightarrow \\operatorname{image}_2 f (\\operatorname{image} g\\ s t) t = (\\operatorname{image}_2 f' s t).\\operatorname{image} g'$$$
Lean4
/-- Symmetric statement to `Set.image_image2_distrib_left`. -/
theorem image2_image_left_comm {f : α' → β → γ} {g : α → α'} {f' : α → β → δ} {g' : δ → γ}
(h_left_comm : ∀ a b, f (g a) b = g' (f' a b)) : image2 f (s.image g) t = (image2 f' s t).image g' :=
(image_image2_distrib_left fun a b => (h_left_comm a b).symm).symm
