bind_comp — Mathlib

English

For a β→. γ and α→. β, and a spooky Part α, the associativity of bind holds: a.bind (f.comp g) = (a.bind g).bind f.

Русский

Для частичных функций, связанных последовательным связыванием, выполняется ассоциативность: a.bind (f.comp g) = (a.bind g).bind f.

LaTeX

$$$$ a\,\text{bind} (f \cdot g) = (a\,\text{bind} g)\,\text{bind} f. $$$$

Lean4

@[simp]
theorem bind_comp (f : β →. γ) (g : α →. β) (a : Part α) : a.bind (f.comp g) = (a.bind g).bind f :=
  by
  ext c
  simp_rw [Part.mem_bind_iff, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]
  rw [exists_comm]
  simp_rw [and_assoc]

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