# 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 each `a` is the max of the occurrences of `a` in `s` and `t`.
- `s ∩ t`: The multiset for which the number of occurrences of each `a` is the min of the occurrences of `a` in `s` and `t`.

### Union #

source
def Multiset.union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
Multiset α

`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

- s.union t = s - t + t

Instances For

source
instance Multiset.instUnion {α : Type u_1} [DecidableEq α] :
Union (Multiset α)
Equations

- Multiset.instUnion = { union := Multiset.union }

source
theorem Multiset.union_def {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ∪ t = s - t + t
source
theorem Multiset.le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s ≤ s ∪ t
source
theorem Multiset.le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
t ≤ s ∪ t
source
theorem Multiset.eq_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
t ≤ s → s ∪ t = s
source
theorem Multiset.union_le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) :
s ∪ u ≤ t ∪ u
source
theorem Multiset.union_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ u) (h₂ : t ≤ u) :
s ∪ t ≤ u
source
@[simp]
theorem Multiset.mem_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
source
@[simp]
theorem Multiset.map_union {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} :
map f (s ∪ t) = map f s ∪ map f t
source
@[simp]
theorem Multiset.zero_union {α : Type u_1} [DecidableEq α] {s : Multiset α} :
0 ∪ s = s
source
@[simp]
theorem Multiset.union_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} :
s ∪ 0 = s
source
@[simp]
theorem Multiset.count_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
count a (s ∪ t) = max (count a s) (count a t)
source
@[simp]
theorem Multiset.filter_union {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
filter p (s ∪ t) = filter p s ∪ filter p t

### Intersection #

source
def Multiset.inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
Multiset α

`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

source
instance Multiset.instInter {α : Type u_1} [DecidableEq α] :
Inter (Multiset α)
Equations

- Multiset.instInter = { inter := Multiset.inter }

source
@[simp]
theorem Multiset.inter_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) :
s ∩ 0 = 0
source
@[simp]
theorem Multiset.zero_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) :
0 ∩ s = 0
source
@[simp]
theorem Multiset.cons_inter_of_pos {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) :
a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a
source
@[simp]
theorem Multiset.cons_inter_of_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) :
a ∉ t → (a ::ₘ s) ∩ t = s ∩ t
source
theorem Multiset.inter_le_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s ∩ t ≤ s
source
theorem Multiset.inter_le_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s ∩ t ≤ t
source
theorem Multiset.le_inter {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u) :
s ≤ t ∩ u
source
@[simp]
theorem Multiset.mem_inter {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} :
a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t
source
instance Multiset.instLattice {α : Type u_1} [DecidableEq α] :
Lattice (Multiset α)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Multiset.sup_eq_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ⊔ t = s ∪ t
source
@[simp]
theorem Multiset.inf_eq_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ⊓ t = s ∩ t
source
@[simp]
theorem Multiset.le_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u
source
@[simp]
theorem Multiset.union_le_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u
source
theorem Multiset.union_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ∪ t = t ∪ s
source
theorem Multiset.inter_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ∩ t = t ∩ s
source
theorem Multiset.eq_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) :
s ∪ t = t
source
theorem Multiset.union_le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) :
u ∪ s ≤ u ∪ t
source
theorem Multiset.union_le_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ∪ t ≤ s + t
source
theorem Multiset.union_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
s ∪ t + u = s + u ∪ (t + u)
source
theorem Multiset.add_union_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
s + (t ∪ u) = s + t ∪ (s + u)
source
theorem Multiset.cons_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
source
theorem Multiset.inter_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
s ∩ t + u = (s + u) ∩ (t + u)
source
theorem Multiset.add_inter_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) :
s + t ∩ u = (s + t) ∩ (s + u)
source
theorem Multiset.cons_inter_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)
source
theorem Multiset.union_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s ∪ t + s ∩ t = s + t
source
theorem Multiset.sub_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s - t + s ∩ t = s
source
theorem Multiset.sub_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s - s ∩ t = s - t
source
@[simp]
theorem Multiset.count_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) :
count a (s ∩ t) = min (count a s) (count a t)
source
@[simp]
theorem Multiset.coe_inter {α : Type u_1} [DecidableEq α] (s t : List α) :
↑s ∩ ↑t = ↑(s.bagInter t)
source
instance Multiset.instDistribLattice {α : Type u_1} [DecidableEq α] :
DistribLattice (Multiset α)
Equations

- Multiset.instDistribLattice = { toLattice := Multiset.instLattice, le_sup_inf := ⋯ }

source
@[simp]
theorem Multiset.filter_inter {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
filter p (s ∩ t) = filter p s ∩ filter p t
source
@[simp]
theorem Multiset.replicate_inter {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α) (s : Multiset α) :
replicate n x ∩ s = replicate (min n (count x s)) x
source
@[simp]
theorem Multiset.inter_replicate {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) (x : α) :
s ∩ replicate n x = replicate (min (count x s) n) x
source
theorem Multiset.inter_add_sub_of_add_eq_add {α : Type u_1} [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) :
N ∩ Q + (P - M) = N

### Disjoint multisets #

source
theorem Multiset.disjoint_left {α : Type u_1} {s t : Multiset α} :
Disjoint s t ↔ ∀ {a : α}, a ∈ s → a ∉ t
source
theorem Disjoint.notMem_of_mem_left_multiset {α : Type u_1} {s t : Multiset α} :
Disjoint s t → ∀ {a : α}, a ∈ s → a ∉ t

Alias of the forward direction of `Multiset.disjoint_left`.

source
@[deprecated Disjoint.notMem_of_mem_left_multiset (since := "2025-05-23")]
theorem Disjoint.not_mem_of_mem_left_multiset {α : Type u_1} {s t : Multiset α} :
Disjoint s t → ∀ {a : α}, a ∈ s → a ∉ t

Alias of the forward direction of `Multiset.disjoint_left`.

Alias of the forward direction of `Multiset.disjoint_left`.

source
@[simp]
theorem Multiset.coe_disjoint {α : Type u_1} (l₁ l₂ : List α) :
Disjoint ↑l₁ ↑l₂ ↔ l₁.Disjoint l₂
source
theorem Multiset.disjoint_right {α : Type u_1} {s t : Multiset α} :
Disjoint s t ↔ ∀ {a : α}, a ∈ t → a ∉ s
source
theorem Disjoint.notMem_of_mem_right_multiset {α : Type u_1} {s t : Multiset α} :
Disjoint s t → ∀ {a : α}, a ∈ t → a ∉ s

Alias of the forward direction of `Multiset.disjoint_right`.

source
@[deprecated Disjoint.notMem_of_mem_right_multiset (since := "2025-05-23")]
theorem Disjoint.not_mem_of_mem_right_multiset {α : Type u_1} {s t : Multiset α} :
Disjoint s t → ∀ {a : α}, a ∈ t → a ∉ s

Alias of the forward direction of `Multiset.disjoint_right`.

Alias of the forward direction of `Multiset.disjoint_right`.

source
theorem Multiset.disjoint_iff_ne {α : Type u_1} {s t : Multiset α} :
Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
source
theorem Multiset.disjoint_of_subset_left {α : Type u_1} {s t u : Multiset α} (h : s ⊆ u) (d : Disjoint u t) :
Disjoint s t
source
theorem Multiset.disjoint_of_subset_right {α : Type u_1} {s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) :
Disjoint s t
source
@[simp]
theorem Multiset.zero_disjoint {α : Type u_1} (l : Multiset α) :
Disjoint 0 l
source
@[simp]
theorem Multiset.singleton_disjoint {α : Type u_1} {l : Multiset α} {a : α} :
Disjoint {a} l ↔ a ∉ l
source
@[simp]
theorem Multiset.disjoint_singleton {α : Type u_1} {l : Multiset α} {a : α} :
Disjoint l {a} ↔ a ∉ l
source
@[simp]
theorem Multiset.disjoint_add_left {α : Type u_1} {s t u : Multiset α} :
Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u
source
@[simp]
theorem Multiset.disjoint_add_right {α : Type u_1} {s t u : Multiset α} :
Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u
source
@[simp]
theorem Multiset.disjoint_cons_left {α : Type u_1} {a : α} {s t : Multiset α} :
Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t
source
@[simp]
theorem Multiset.disjoint_cons_right {α : Type u_1} {a : α} {s t : Multiset α} :
Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t
source
theorem Multiset.inter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s ∩ t = 0 ↔ Disjoint s t
source
@[simp]
theorem Multiset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
source
@[simp]
theorem Multiset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} :
Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
source
theorem Multiset.add_eq_union_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
s + t = s ∪ t ↔ Disjoint s t
source
theorem Multiset.add_eq_union_left_of_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h : t ≤ s) :
u + s = u ∪ t ↔ Disjoint u s ∧ s = t
source
theorem Multiset.add_eq_union_right_of_le {α : Type u_1} [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) :
x + y = x ∪ z ↔ y = z ∧ Disjoint x y
source
theorem Multiset.disjoint_map_map {α : Type u_1} {β : Type v} {γ : Type u_2} {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} :
Disjoint (map f s) (map g t) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
source
theorem Multiset.map_set_pairwise {α : Type u_1} {β : Type v} {f : α → β} {r : β → β → Prop} {m : Multiset α} (h : {a : α | a ∈ m}.Pairwise fun (a₁ a₂ : α) => r (f a₁) (f a₂)) :
{b : β | b ∈ map f m}.Pairwise r
source
theorem Multiset.nodup_add {α : Type u_1} {s t : Multiset α} :
(s + t).Nodup ↔ s.Nodup ∧ t.Nodup ∧ Disjoint s t
source
theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s t : Multiset α} (d : (s + t).Nodup) :
Disjoint s t
source
theorem Multiset.Nodup.add_iff {α : Type u_1} {s t : Multiset α} (d₁ : s.Nodup) (d₂ : t.Nodup) :
(s + t).Nodup ↔ Disjoint s t
source
theorem Multiset.Nodup.inter_left {α : Type u_1} {s : Multiset α} [DecidableEq α] (t : Multiset α) :
s.Nodup → (s ∩ t).Nodup
source
theorem Multiset.Nodup.inter_right {α : Type u_1} {t : Multiset α} [DecidableEq α] (s : Multiset α) :
t.Nodup → (s ∩ t).Nodup
source
@[simp]
theorem Multiset.nodup_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} :
(s ∪ t).Nodup ↔ s.Nodup ∧ t.Nodup