English
If a is a left identity for f: α → γ → γ (i.e., f a b = b for all b), then image₂ f {a} t = t for any Finset t.
Русский
Пусть a является левым нейтралом для f: α → γ → γ (т. е. f a b = b для всех b). Тогда image₂ f {a} t = t для любого Finset t.
LaTeX
$$$\\forall f:\\alpha\\to\\gamma\\to\\gamma\\,\\forall a:\\alpha\\, (\\forall b:\\gamma, f\\ a\\ b = b)\\Rightarrow image_2 f \\{a\\} \\; t = t$$$
Lean4
/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Finset.image₂ f`. -/
theorem image₂_left_identity {f : α → γ → γ} {a : α} (h : ∀ b, f a b = b) (t : Finset γ) : image₂ f { a } t = t :=
coe_injective <| by rw [coe_image₂, coe_singleton, Set.image2_left_identity h]
