map₂_left_identity — Mathlib

English

If f is left identity on β, i.e., f a b = b for a fixed a, then some a is a left identity for map₂ f: map₂ f (some a) o = o for any option o of type β.

Русский

Если есть элемент a такой, что f a b = b для всех b, тогда some a является левым единичным элементом для map₂ f: map₂ f (some a) o = o для любого o ∈ Option β.

LaTeX

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

Lean4

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

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