bind_ret — Mathlib

English

The operation bind with a function of the form ret ∘ f collapses to map f after binding, i.e., bind s (ret ∘ f) ~ʷ map f s.

Русский

Операция bind с функцией вида ret ∘ f сводится к map f после bind: bind s (ret ∘ f) ~ʷ map f s.

LaTeX

$$$ \forall f : \alpha \to \mathrm{WSeq}\,\beta,\; s : \mathrm{WSeq}\,\alpha,\; \mathrm{bind}\ s (\mathrm{ret} \circ f) ~ʷ \mathrm{map}\; f\; s$$$

Lean4

@[simp]
theorem bind_ret (f : α → β) (s) : bind s (ret ∘ f) ~ʷ map f s :=
  by
  dsimp [bind]
  rw [map_comp]
  apply join_map_ret

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