Theorems · Definition · combinatorics

Multiset.join

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

join S, where S is a multiset of multisets, is the lift of the list join operation, that is, the union of all the sets. For example, join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}.

Defined in

Mathlib.Data.Multiset.Bind

Cited by

21 results in Mathlib

Foundations

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