Theorems · Definition · combinatorics

Multiset.bind

{α : Type u_1} → {β : Type v} → Multiset α → (α → Multiset β) → Multiset β

s.bind f is the monad bind operation, defined as (s.map f).join. It is the union of f a as a ranges over s.

Defined in

Mathlib.Data.Multiset.Bind

Cited by

59 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound