pure_bind — Mathlib

English

For any f: α → FreeGroup β and any x, pure x >>= f = f x. This is the left identity law for the FreeGroup monad.

Русский

Для любой функции f: α → FreeGroup β и любого элемента x, выполняется чистый x >>= f = f x. Это левая единица монадического закона для свободной группы.

LaTeX

$$$$ (\\text{pure } x) \\gg= f = f x. $$$$

Lean4

@[to_additive]
theorem pure_bind (f : α → FreeGroup β) (x) : pure x >>= f = f x :=
  lift_apply_of

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