pure_bind — Mathlib

English

For any f : α → FreeAbelianGroup β and x ∈ α, pure x >>= f = f x; i.e., lifting the unit commutes with bind.

Русский

Для любого f : α → FreeAbelianGroup β и x ∈ α, чистый элемент x связываетc с f x; т.е. привязка чистого элемента к f равна f x.

LaTeX

$$$ \forall {\alpha \beta} (f : \alpha \to FreeAbelianGroup(\beta)) (x : \alpha),\; \text{pure } x >>= f = f x$$$

Lean4

theorem pure_bind (f : α → FreeAbelianGroup β) (x) : pure x >>= f = f x :=
  lift_apply_of _ _

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