image₂_right_identity — Mathlib

English

If b is a right identity for f: γ → β → γ (i.e., f a b = a for all a), then image₂ f s {b} = s for any Finset s.

Русский

Пусть b является правым нейтралом для f: γ → β → γ (то есть f a b = a). Тогда image₂ f s {b} = s для любого Finset s.

LaTeX

$$$\\forall f:\\gamma\\to\\beta\\to\\gamma\\,\\forall b:\\beta, (\\forall a:\\gamma, f\\ a\\ b = a)\\Rightarrow image_2 f s \\{b\\} = s$$$

Lean4

/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Finset.image₂ f`. -/
theorem image₂_right_identity {f : γ → β → γ} {b : β} (h : ∀ a, f a b = a) (s : Finset γ) : image₂ f s { b } = s := by
  rw [image₂_singleton_right, funext h, image_id']

Похожие утверждения