map₂_left_identity — Mathlib

English

If f(a, b) = b for all b, then map₂ f (pure a) l = l for any filter l.

Русский

Если f(a, b) = b для всех b, тогда map₂ f (pure a) l = l для любого фильтра l.

LaTeX

$$$\big(\forall b,\ f\ a\ b = b\big) \Rightarrow \forall l,\ map_2 f (\mathrm{pure} a) l = l$$$

Lean4

/-- If `a` is a left identity for `f : α → β → β`, then `pure a` is a left identity for
`Filter.map₂ f`. -/
theorem map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (l : Filter β) : map₂ f (pure a) l = l := by
  rw [map₂_pure_left, show f a = id from funext h, map_id]

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