map₂_right_identity — Mathlib

English

If b is a right identity for a binary operation f, i.e., f a b = a for all a, then map₂ f o (some b) = o for all o.

Русский

Если b является правым единичным элементом для операции f, то map₂ f o (some b) = o для любого o.

LaTeX

$$$\\forall a\\, (\\forall b, f a b = a) \\Rightarrow map\_2 f o (some b) = o$$$

Lean4

/-- If `b` is a right identity for a binary operation `f`, then `some b` is a right identity for
`Option.map₂ f`. -/
theorem map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (o : Option α) : map₂ f o (some b) = o := by
  grind

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