map_bind' — Mathlib

English

Mapping f over the result of binding x with g equals binding x with the map of f over g.

Русский

Преобразование через map над результатом связывания равняется связыванию, где к каждому элементу применяется map.

LaTeX

$$$$ \mathrm{Option.map} f (x \bind g) = x \bind (\lambda a, \mathrm{Option.map} f (g a)). $$$$

Lean4

@[deprecated map_bind (since := "2025-04-10")]
theorem map_bind' (f : β → γ) (x : Option α) (g : α → Option β) :
    Option.map f (x.bind g) = x.bind fun a ↦ Option.map f (g a) :=
  map_bind

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