English
Symmetric form: if g(f(a,b)) = f'(a,b) with a a left-argument mapping, then (image2 f s t).image g = image2 f' (s.image g') t.
Русский
Симметричная форма: если распределение слева выполняется, то (image2 f s t).image g = image2 f' (s.image g') t.
LaTeX
$$$\\forall a b,\\ g(f(a,b)) = f'(a,b) \\Rightarrow (\\operatorname{image}_2 f\\ s\\ t).\\operatorname{image} g = \\operatorname{image}_2 f' (\\operatorname{image} g'\\ s) t$$$
Lean4
/-- Symmetric statement to `Set.image2_image_left_comm`. -/
theorem image_image2_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
(h_distrib : ∀ a b, g (f a b) = f' (g' a) b) : (image2 f s t).image g = image2 f' (s.image g') t :=
(image_image2_distrib h_distrib).trans <| by rw [image_id']
