Distributive lattice structure on multisets #
This file defines an instance DistribLattice (Multiset α)
using the union and intersection
operators:
s ∪ t
: The multiset for which the number of occurrences of eacha
is the max of the occurrences ofa
ins
andt
.s ∩ t
: The multiset for which the number of occurrences of eacha
is the min of the occurrences ofa
ins
andt
.
Union #
s ∪ t
is the multiset such that the multiplicity of each a
in it is the maximum of the
multiplicity of a
in s
and t
. This is the supremum of multisets.
Equations
Instances For
Intersection #
s ∩ t
is the multiset such that the multiplicity of each a
in it is the minimum of the
multiplicity of a
in s
and t
. This is the infimum of multisets.
Equations
Instances For
Equations
Disjoint multisets #
Alias of the forward direction of Multiset.disjoint_left
.
Alias of the forward direction of Multiset.disjoint_left
.
Alias of the forward direction of Multiset.disjoint_left
.
Alias of Disjoint.symm
.
Alias of disjoint_comm
.
Alias of the forward direction of Multiset.disjoint_right
.
Alias of the forward direction of Multiset.disjoint_right
.
Alias of the forward direction of Multiset.disjoint_right
.
Alias of Disjoint.mono_left
.
Alias of Disjoint.mono_right
.