image2_right_identity — Mathlib

English

If b is a right identity for f: α × β → α, then {b} is a right identity for image2 f: image2 f s {b} = s for any s.

Русский

Если b является правым тождественным для f: α × β → α, тогда {b} является правым тождественным для image2: image2 f s {b} = s для любого s.

LaTeX

$$$\\forall s,\\ image2 f s {b} = s$ при условии $\\forall a, f a b = a$.$$

Lean4

/-- If `b` is a right identity for `f : α → β → α`, then `{b}` is a right identity for
`Set.image2 f`. -/
theorem image2_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (s : Set α) : image2 f s { b } = s := by
  rw [image2_singleton_right, funext h, image_id']

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