map_bind — Mathlib

English

Mapping after binding equals binding after mapping: map f (bind m n) = bind m (λ a, map f (n a)).

Русский

Отображение после связывания равно связыванию после отображения: map f (bind m n) = bind m (λ a, map f (n a)).

LaTeX

$$$\\mathrm{map}\, f\\,(\\mathrm{bind}\\, m\\, n) = \\mathrm{bind}\\, m (\\lambda a. \\mathrm{map}\\, f\\,(n\\, a))$$$

Lean4

theorem map_bind (m : Multiset α) (n : α → Multiset β) (f : β → γ) : map f (bind m n) = bind m fun a => map f (n a) :=
  by simp [bind]

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