map₂_right_identity — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `b` is a right identity for `f : α → β → α`, then `pure b` is a right identity for
`Filter.map₂ f`. -/
theorem map₂_right_identity {f : α → β → α} {b : β} (h : ∀ a, f a b = a) (l : Filter α) : map₂ f l (pure b) = l := by
  rw [map₂_pure_right, funext h, map_id']

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