English
Variant symmetric to image2_image_left_anticomm: if f (g a) b = g' (f' b a), then image2 f (s.image g) t = image2 g' (image2 f' t s).
Русский
Вариант симметрии к антикоммутативности слева: если f(g a) b = g'(f' b a), то image2 f (s.image g) t = image2 g' (image2 f' t s).
LaTeX
$$$\\forall a b,\\ f (g a) b = g'(f' b a) \\Rightarrow \\operatorname{image}_2 f (s \\ image g) t = \\operatorname{image}_2 g' (\\operatorname{image}_2 f' t s)$$$
Lean4
/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Set.image2 f`. -/
theorem image2_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (t : Set β) : image2 f { a } t = t := by
rw [image2_singleton_left, show f a = id from funext h, image_id]
