sub_bind — Mathlib

English

Subtract distributes under bind: (x - y) >>= f = (x >>= f) - (y >>= f).

Русский

Вычитание распределяется под привязкой: (x - y) >>= f = (x >>= f) - (y >>= f).

LaTeX

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

Lean4

@[simp]
theorem sub_bind (f : α → FreeAbelianGroup β) (x y : FreeAbelianGroup α) : x - y >>= f = (x >>= f) - (y >>= f) :=
  map_sub (lift f) _ _

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