English
Symmetric form of image_image2_antidistrib: image g (image2 f s t) = image2 f (t.image g) s under a suitable left-antidistributive law.
Русский
Симметричная форма антираспределения слева: image g (image2 f s t) = image2 f (t.image g) s при подходящем левом антираспределении.
LaTeX
$$$\\forall s t,\\ \\operatorname{image} g (\\operatorname{image}_2 f s t) = \\operatorname{image}_2 f (t \\ image g) s$$$
Lean4
/-- Symmetric statement to `Set.image2_image_left_anticomm`. -/
theorem image_image2_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
(h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) : (image2 f s t).image g = image2 f' (t.image g') s :=
(image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']
