bind_map — Mathlib

English

Mapping f over x and then binding with g equals binding over x with the mapped g.

Русский

Отображение по f над x, затем связывание с g эквивалентно связыванию над x с отображением g.

LaTeX

$$$ (\operatorname{map} f\, x).\bind g = x.\bind (\\lambda y, g (f y)) $$$

Lean4

@[simp]
theorem bind_map {γ} (f : α → β) (x) (g : β → Part γ) : (map f x).bind g = x.bind fun y => g (f y) := by
  rw [← bind_some_eq_map, bind_assoc]; simp

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