Skip to content

Rename multiset "union" into "disjoint union"

Robbert Krebbers requested to merge robbert/disj_union into master

This fixes #13 (closed). Now ∪ and ∩ are the usual multiset union and intersection (i.e. taking max and min, respectively), whereas ⊎ is the "sum" (i.e. adding the multiplicities).

Some questions/remarks:

  • ⊎ and ∪ have different heights in my font (see ⊎∪). Is there maybe a better disjoint union symbol in unicode?
  • There are probably all kinds of laws about the interaction between ∪, ∩, and ⊎, like distributivity. I did not attempt to prove a comprehensive set of such laws.
  • ∖ is still the operation that subtracts multiplicity. I think that's fine, since there is no sensible difference operator for multisets that matches up with the union operator.

Merge request reports