English
Symmetric statement to image2_antidistrib_right: image2 f s (image g t) = image2 f s t.image g with an appropriate antih distribution condition.
Русский
Симметрия к антираспределению справа: image2 f s (image g t) = image2 f s t.image g при подходящем условии антираспределения.
LaTeX
$$$\\forall s t,\\ image2 f s (image g t) = image2 f s (t \\ image g)$$$
Lean4
/-- Symmetric statement to `Set.image_image2_antidistrib_right`. -/
theorem image_image2_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
(h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) : image2 f s (t.image g) = (image2 f' t s).image g' :=
(image_image2_antidistrib_right fun a b => (h_right_anticomm b a).symm).symm
