English
Associativity of bind up to composition: bind (bind s f) g is equivalent to bind s ( (fun y => y.bind g) ∘ f ).
Русский
Ассоциативность bind с точностью до композиции: bind (bind s f) g эквивалентно bind s ( (fun y => y.bind g) ∘ f ).
LaTeX
$$$ \forall s : \mathrm{WSeq}\,\alpha,\; f : \alpha \to \mathrm{WSeq}\,\beta,\; g : \beta \to \mathrm{WSeq}\,\gamma,\; \mathrm{bind}(\mathrm{bind}\ s f) g ~ʷ \mathrm{bind}\ s ((\mathrm{fun}\ y : \mathrm{WSeq}\,\beta => \mathrm{bind}\ y g) \circ f)$$$
Lean4
@[simp]
theorem bind_assoc (s : WSeq α) (f : α → WSeq β) (g : β → WSeq γ) :
bind (bind s f) g ~ʷ bind s fun x : α => bind (f x) g := by exact bind_assoc_comp s f g
