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

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

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

Equations

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

theorem Multiset.union_def {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t = s - t + t

theorem Multiset.le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ≤ s ∪ t

theorem Multiset.le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s ∪ t

theorem Multiset.eq_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : t ≤ s → s ∪ t = s

theorem Multiset.union_le_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) : s ∪ u ≤ t ∪ u

theorem Multiset.union_le {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u

@[simp]

theorem Multiset.mem_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t

@[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

@[simp]

theorem Multiset.zero_union {α : Type u_1} [DecidableEq α] {s : Multiset α} : 0 ∪ s = s

@[simp]

theorem Multiset.union_zero {α : Type u_1} [DecidableEq α] {s : Multiset α} : s ∪ 0 = s

@[simp]

theorem Multiset.count_union {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t)

@[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

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₂)) ⋯

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

Equations

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

@[simp]

theorem Multiset.inter_zero {α : Type u_1} [DecidableEq α] (s : Multiset α) : s ∩ 0 = 0

@[simp]

theorem Multiset.zero_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) : 0 ∩ s = 0

@[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

@[simp]

theorem Multiset.cons_inter_of_neg {α : Type u_1} [DecidableEq α] {t : Multiset α} {a : α} (s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t

theorem Multiset.inter_le_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t ≤ s

theorem Multiset.inter_le_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t ≤ t

theorem Multiset.le_inter {α : Type u_1} [DecidableEq α] {s t u : Multiset α} (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u

@[simp]

theorem Multiset.mem_inter {α : Type u_1} [DecidableEq α] {s t : Multiset α} {a : α} : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t

instance Multiset.instLattice {α : Type u_1} [DecidableEq α] : Lattice (Multiset α)

Equations

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

@[simp]

theorem Multiset.sup_eq_union {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ⊔ t = s ∪ t

@[simp]

theorem Multiset.inf_eq_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ⊓ t = s ∩ t

@[simp]

theorem Multiset.le_inter_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u

@[simp]

theorem Multiset.union_le_iff {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u

theorem Multiset.union_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t = t ∪ s

theorem Multiset.inter_comm {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∩ t = t ∩ s

theorem Multiset.eq_union_right {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) : s ∪ t = t

theorem Multiset.union_le_union_left {α : Type u_1} [DecidableEq α] {s t : Multiset α} (h : s ≤ t) (u : Multiset α) : u ∪ s ≤ u ∪ t

theorem Multiset.union_le_add {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t ≤ s + t

theorem Multiset.union_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u)

theorem Multiset.add_union_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u)

theorem Multiset.cons_union_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

theorem Multiset.inter_add_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u)

theorem Multiset.add_inter_distrib {α : Type u_1} [DecidableEq α] (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u)

theorem Multiset.cons_inter_distrib {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

theorem Multiset.union_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s ∪ t + s ∩ t = s + t

theorem Multiset.sub_add_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - t + s ∩ t = s

theorem Multiset.sub_inter {α : Type u_1} [DecidableEq α] (s t : Multiset α) : s - s ∩ t = s - t

@[simp]

theorem Multiset.count_inter {α : Type u_1} [DecidableEq α] (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t)

@[simp]

theorem Multiset.coe_inter {α : Type u_1} [DecidableEq α] (s t : List α) : ↑s ∩ ↑t = ↑(s.bagInter t)

instance Multiset.instDistribLattice {α : Type u_1} [DecidableEq α] : DistribLattice (Multiset α)

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 α) : filter p (s ∩ t) = filter p s ∩ filter p t

@[simp]

theorem Multiset.replicate_inter {α : Type u_1} [DecidableEq α] (n : ℕ) (x : α) (s : Multiset α) : replicate n x ∩ s = replicate (min n (count x s)) x

@[simp]

theorem Multiset.inter_replicate {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) (x : α) : s ∩ replicate n x = replicate (min (count x s) n) x

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

@[deprecated Disjoint (since := "2024-11-01")]

def Multiset.Disjoint {α : Type u_1} (s t : Multiset α) : Prop

Disjoint s t means that s and t have no elements in common.

Equations

• s.Disjoint t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t → False

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

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.

@[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.

@[simp]

theorem Multiset.coe_disjoint {α : Type u_1} (l₁ l₂ : List α) : Disjoint ↑l₁ ↑l₂ ↔ l₁.Disjoint l₂

@[deprecated Disjoint.symm (since := "2024-11-01")]

theorem Multiset.Disjoint.symm {α : Type u_1} [PartialOrder α] [OrderBot α] ⦃a b : α⦄ : Disjoint a b → Disjoint b a

Alias of Disjoint.symm.

@[deprecated disjoint_comm (since := "2024-11-01")]

theorem Multiset.disjoint_comm {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} : Disjoint a b ↔ Disjoint b a

Alias of disjoint_comm.

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

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.

@[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.

theorem Multiset.disjoint_iff_ne {α : Type u_1} {s t : Multiset α} : Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

theorem Multiset.disjoint_of_subset_left {α : Type u_1} {s t u : Multiset α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t

theorem Multiset.disjoint_of_subset_right {α : Type u_1} {s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

@[deprecated Disjoint.mono_left (since := "2024-11-01")]

theorem Multiset.disjoint_of_le_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} (h : a ≤ b) : Disjoint b c → Disjoint a c

Alias of Disjoint.mono_left.

@[deprecated Disjoint.mono_right (since := "2024-11-01")]

theorem Multiset.disjoint_of_le_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} : b ≤ c → Disjoint a c → Disjoint a b

Alias of Disjoint.mono_right.

@[simp]

theorem Multiset.zero_disjoint {α : Type u_1} (l : Multiset α) : Disjoint 0 l

@[simp]

theorem Multiset.singleton_disjoint {α : Type u_1} {l : Multiset α} {a : α} : Disjoint {a} l ↔ a ∉ l

@[simp]

theorem Multiset.disjoint_singleton {α : Type u_1} {l : Multiset α} {a : α} : Disjoint l {a} ↔ a ∉ l

@[simp]

theorem Multiset.disjoint_add_left {α : Type u_1} {s t u : Multiset α} : Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Multiset.disjoint_add_right {α : Type u_1} {s t u : Multiset α} : Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u

@[simp]

theorem Multiset.disjoint_cons_left {α : Type u_1} {a : α} {s t : Multiset α} : Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t

@[simp]

theorem Multiset.disjoint_cons_right {α : Type u_1} {a : α} {s t : Multiset α} : Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t

theorem Multiset.inter_eq_zero_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s ∩ t = 0 ↔ Disjoint s t

@[simp]

theorem Multiset.disjoint_union_left {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Multiset.disjoint_union_right {α : Type u_1} [DecidableEq α] {s t u : Multiset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

theorem Multiset.add_eq_union_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Multiset α} : s + t = s ∪ t ↔ Disjoint s t

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

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

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

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

theorem Multiset.nodup_add {α : Type u_1} {s t : Multiset α} : (s + t).Nodup ↔ s.Nodup ∧ t.Nodup ∧ Disjoint s t

theorem Multiset.disjoint_of_nodup_add {α : Type u_1} {s t : Multiset α} (d : (s + t).Nodup) : Disjoint s t

theorem Multiset.Nodup.add_iff {α : Type u_1} {s t : Multiset α} (d₁ : s.Nodup) (d₂ : t.Nodup) : (s + t).Nodup ↔ Disjoint s t

theorem Multiset.Nodup.inter_left {α : Type u_1} {s : Multiset α} [DecidableEq α] (t : Multiset α) : s.Nodup → (s ∩ t).Nodup

theorem Multiset.Nodup.inter_right {α : Type u_1} {t : Multiset α} [DecidableEq α] (s : Multiset α) : t.Nodup → (s ∩ t).Nodup

@[simp]

theorem Multiset.nodup_union {α : Type u_1} [DecidableEq α] {s t : Multiset α} : (s ∪ t).Nodup ↔ s.Nodup ∧ t.Nodup