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.
Instances For
Equations
- Multiset.instUnion = { union := Multiset.union }
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
- s.inter t = Quotient.liftOn₂ s t (fun (l₁ l₂ : List α) => ↑(l₁.bagInter l₂)) ⋯
Instances For
Equations
- Multiset.instInter = { inter := Multiset.inter }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Multiset.instDistribLattice = { toLattice := Multiset.instLattice, le_sup_inf := ⋯ }
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
.