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 }
theorem
Multiset.union_le_union_right
{α : Type u_1}
[DecidableEq α]
{s t : Multiset α}
(h : s ≤ t)
(u : Multiset α)
:
theorem
Multiset.union_le
{α : Type u_1}
[DecidableEq α]
{s t u : Multiset α}
(h₁ : s ≤ u)
(h₂ : t ≤ u)
:
@[simp]
theorem
Multiset.map_union
{α : Type u_1}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
{f : α → β}
(finj : Function.Injective f)
{s t : Multiset α}
:
@[simp]
@[simp]
@[simp]
theorem
Multiset.filter_union
{α : Type u_1}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(s t : Multiset α)
:
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 }
@[simp]
@[simp]
@[simp]
theorem
Multiset.cons_inter_of_neg
{α : Type u_1}
[DecidableEq α]
{t : Multiset α}
{a : α}
(s : Multiset α)
:
theorem
Multiset.le_inter
{α : Type u_1}
[DecidableEq α]
{s t u : Multiset α}
(h₁ : s ≤ t)
(h₂ : s ≤ u)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
theorem
Multiset.union_le_union_left
{α : Type u_1}
[DecidableEq α]
{s t : Multiset α}
(h : s ≤ t)
(u : Multiset α)
:
@[simp]
Equations
- Multiset.instDistribLattice = { toLattice := Multiset.instLattice, le_sup_inf := ⋯ }
@[simp]
theorem
Multiset.filter_inter
{α : Type u_1}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(s t : Multiset α)
:
Disjoint multisets #
Alias of the forward direction of Multiset.disjoint_left
.
@[deprecated Disjoint.notMem_of_mem_left_multiset (since := "2025-05-23")]
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_right
.
@[deprecated Disjoint.notMem_of_mem_right_multiset (since := "2025-05-23")]
Alias of the forward direction of Multiset.disjoint_right
.
Alias of the forward direction of Multiset.disjoint_right
.
theorem
Multiset.Nodup.inter_left
{α : Type u_1}
{s : Multiset α}
[DecidableEq α]
(t : Multiset α)
:
theorem
Multiset.Nodup.inter_right
{α : Type u_1}
{t : Multiset α}
[DecidableEq α]
(s : Multiset α)
: