map_bind — Mathlib

English

Mapping g over the result of a bind is the same as binding with the map of g after f.

Русский

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

LaTeX

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

Lean4

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

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