doc-next-gen

Mathlib.Data.Multiset.UnionInter

Module docstring

{"# 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 ","### Intersection ","### Disjoint multisets "}
Multiset.union definition
(s t : Multiset α) : Multiset α
Full source 
/-- `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. -/
def union (s t : Multiset α) : Multiset α := s - t + t
Union of multisets
Informal description
For two multisets \( s \) and \( t \) over a type \( \alpha \), the union \( s \cup t \) is defined as the multiset where each element \( a \) appears with multiplicity equal to the maximum of its multiplicities in \( s \) and \( t \). This operation is implemented as \( s \setminus t + t \), where \( s \setminus t \) denotes the multiset difference.
Multiset.instUnion instance
: Union (Multiset α)
Full source 
instance : Union (Multiset α) :=
  ⟨union⟩
Union Operation on Multisets
Informal description
For any type $\alpha$, the multiset over $\alpha$ has a union operation $\cup$ defined such that for two multisets $s$ and $t$, the multiplicity of each element $a$ in $s \cup t$ is the maximum of its multiplicities in $s$ and $t$.
Multiset.union_def theorem
(s t : Multiset α) : s ∪ t = s - t + t
Full source 
lemma union_def (s t : Multiset α) : s ∪ t = s - t + t := rfl
Union of Multisets as Sum of Difference and Second Multiset
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the union $s \cup t$ is equal to the sum of the multiset difference $s \setminus t$ and $t$.
Multiset.le_union_left theorem
: s ≤ s ∪ t
Full source 
lemma le_union_left : s ≤ s ∪ t := Multiset.le_sub_add
Submultiset Property of Left Union in Multisets
Informal description
For any multiset $s$ and $t$ over a type $\alpha$, the multiset $s$ is a submultiset of the union $s \cup t$.
Multiset.le_union_right theorem
: t ≤ s ∪ t
Full source 
lemma le_union_right : t ≤ s ∪ t := le_add_left _ _
Submultiset Property of Right Union in Multisets
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the multiset $t$ is a submultiset of the union $s \cup t$.
Multiset.union_le theorem
(h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u
Full source 
lemma union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by
  rw [← eq_union_left h₂]; exact union_le_union_right h₁ t
Union of Submultisets is a Submultiset
Informal description
For any multisets $s$, $t$, and $u$, if $s \leq u$ and $t \leq u$, then the union $s \cup t \leq u$.
Multiset.mem_union theorem
: a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
Full source 
@[simp]
lemma mem_union : a ∈ s ∪ ta ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t :=
  ⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _),
    (Or.elim · (mem_of_le le_union_left) (mem_of_le le_union_right))⟩
Membership in Union of Multisets: $a \in s \cup t \leftrightarrow a \in s \lor a \in t$
Informal description
For any element $a$ and multisets $s$ and $t$ over a type $\alpha$, the element $a$ belongs to the union $s \cup t$ if and only if $a$ belongs to $s$ or $a$ belongs to $t$.
Multiset.map_union theorem
[DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} : map f (s ∪ t) = map f s ∪ map f t
Full source 
@[simp]
lemma map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} :
    map f (s ∪ t) = mapmap f s ∪ map f t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ =>
    congr_arg ofList (by rw [List.map_append, List.map_diff finj])
Image of Multiset Union Under Injective Map Equals Union of Images
Informal description
Let $\alpha$ and $\beta$ be types with decidable equality on $\beta$, and let $f : \alpha \to \beta$ be an injective function. For any multisets $s, t$ over $\alpha$, the image of their union under $f$ equals the union of their images, i.e., \[ \text{map}\, f (s \cup t) = \text{map}\, f\, s \cup \text{map}\, f\, t. \]
Multiset.zero_union theorem
: 0 ∪ s = s
Full source 
@[simp] lemma zero_union : 0 ∪ s = s := by simp [union_def, Multiset.zero_sub]
Left Identity of Union with Empty Multiset
Informal description
For any multiset $s$ over a type $\alpha$, the union of the empty multiset $0$ with $s$ is equal to $s$, i.e., $0 \cup s = s$.
Multiset.union_zero theorem
: s ∪ 0 = s
Full source 
@[simp] lemma union_zero : s ∪ 0 = s := by simp [union_def]
Right Identity of Union with Empty Multiset
Informal description
For any multiset $s$ over a type $\alpha$, the union of $s$ with the empty multiset $0$ is equal to $s$, i.e., $s \cup 0 = s$.
Multiset.count_union theorem
(a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t)
Full source 
@[simp]
lemma count_union (a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t) := by
  simp [(· ∪ ·), union, Nat.sub_add_eq_max]
Count of Element in Union of Multisets Equals Maximum of Counts
Informal description
For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the count of $a$ in the union $s \cup t$ is equal to the maximum of the counts of $a$ in $s$ and $t$, i.e., $$\text{count}(a, s \cup t) = \max(\text{count}(a, s), \text{count}(a, t)).$$
Multiset.filter_union theorem
(p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∪ t) = filter p s ∪ filter p t
Full source 
@[simp] lemma filter_union (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
    filter p (s ∪ t) = filterfilter p s ∪ filter p t := by simp [(· ∪ ·), union]
Filtering Commutes with Union in Multisets
Informal description
For any decidable predicate $p$ on elements of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the filter of the union $s \cup t$ under $p$ is equal to the union of the filters of $s$ and $t$ under $p$, i.e., \[ \mathrm{filter}\, p\, (s \cup t) = \mathrm{filter}\, p\, s \cup \mathrm{filter}\, p\, t. \]
Multiset.inter definition
(s t : Multiset α) : Multiset α
Full source 
/-- `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. -/
def inter (s t : Multiset α) : Multiset α :=
  Quotient.liftOn₂ s t (fun l₁ l₂ => (l₁.bagInter l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ =>
    Quot.sound <| p₁.bagInter p₂
Intersection of multisets
Informal description
The intersection of two multisets \( s \) and \( t \), denoted \( s \cap t \), is the multiset where the multiplicity of each element \( a \) is the minimum of its multiplicities in \( s \) and \( t \). This defines the infimum operation in the lattice structure on multisets.
Multiset.instInter instance
: Inter (Multiset α)
Full source 
instance : Inter (Multiset α) := ⟨inter⟩
Intersection Operation on Multisets
Informal description
For any type $\alpha$, the multiset over $\alpha$ has an intersection operation $\cap$ defined by taking the minimum multiplicity for each element.
Multiset.inter_zero theorem
(s : Multiset α) : s ∩ 0 = 0
Full source 
@[simp] lemma inter_zero (s : Multiset α) : s ∩ 0 = 0 :=
  Quot.inductionOn s fun l => congr_arg ofList l.bagInter_nil
Intersection with Empty Multiset Yields Empty Multiset
Informal description
For any multiset $s$ over a type $\alpha$, the intersection of $s$ with the empty multiset is the empty multiset, i.e., $s \cap 0 = 0$.
Multiset.zero_inter theorem
(s : Multiset α) : 0 ∩ s = 0
Full source 
@[simp] lemma zero_inter (s : Multiset α) : 0 ∩ s = 0 :=
  Quot.inductionOn s fun l => congr_arg ofList l.nil_bagInter
Empty Multiset Intersection Identity: $0 \cap s = 0$
Informal description
For any multiset $s$ over a type $\alpha$, the intersection of the empty multiset with $s$ is the empty multiset, i.e., $0 \cap s = 0$.
Multiset.cons_inter_of_pos theorem
(s : Multiset α) : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a
Full source 
@[simp]
lemma cons_inter_of_pos (s : Multiset α) : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_pos _ h
Intersection with Multiset Addition of Member Element
Informal description
For any multiset $s$ over a type $\alpha$ and any element $a$ that is a member of multiset $t$, the intersection of the multiset $a ::ₘ s$ (formed by adding $a$ to $s$) with $t$ is equal to $a$ added to the intersection of $s$ with the multiset obtained by removing one occurrence of $a$ from $t$. That is, $(a ::ₘ s) \cap t = a ::ₘ (s \cap t.erase a)$.
Multiset.cons_inter_of_neg theorem
(s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t
Full source 
@[simp]
lemma cons_inter_of_neg (s : Multiset α) : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_neg _ h
Intersection with Multiset Addition of Non-Member Element
Informal description
For any multiset $s$ over a type $\alpha$ and any element $a \notin t$, the intersection of the multiset $a ::ₘ s$ (formed by adding $a$ to $s$) with $t$ is equal to the intersection of $s$ with $t$. That is, $(a ::ₘ s) \cap t = s \cap t$.
Multiset.inter_le_left theorem
: s ∩ t ≤ s
Full source 
lemma inter_le_left : s ∩ t ≤ s :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => (bagInter_sublist_left _ _).subperm
Intersection is a Submultiset of the Left Operand
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ is a submultiset of $s$, i.e., $s \cap t \leq s$.
Multiset.inter_le_right theorem
: s ∩ t ≤ t
Full source 
lemma inter_le_right : s ∩ t ≤ t := by
  induction s using Multiset.induction_on generalizing t with
  | empty => exact (zero_inter t).symm ▸ zero_le _
  | cons a s IH =>
    by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]
Intersection is a Submultiset of the Right Operand
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ is a submultiset of $t$, i.e., $s \cap t \leq t$.
Multiset.le_inter theorem
(h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u
Full source 
lemma le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u := by
  revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂
  · simpa only [zero_inter] using h₁
  by_cases h : a ∈ u
  · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons]
    exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂)
  · rw [cons_inter_of_neg _ h]
    exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂
Submultiset Property of Intersection: $s \leq t \cap u$ given $s \leq t$ and $s \leq u$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, if $s$ is a submultiset of $t$ and $s$ is a submultiset of $u$, then $s$ is a submultiset of the intersection $t \cap u$.
Multiset.mem_inter theorem
: a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t
Full source 
@[simp]
lemma mem_inter : a ∈ s ∩ ta ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t :=
  ⟨fun h => ⟨mem_of_le inter_le_left h, mem_of_le inter_le_right h⟩, fun ⟨h₁, h₂⟩ => by
    rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩
Membership in Multiset Intersection
Informal description
For any element $a$ and multisets $s$ and $t$ over a type $\alpha$, the element $a$ belongs to the intersection $s \cap t$ if and only if $a$ belongs to both $s$ and $t$. That is, $a \in s \cap t \leftrightarrow a \in s \land a \in t$.
Multiset.instLattice instance
: Lattice (Multiset α)
Full source 
instance instLattice : Lattice (Multiset α) where
  sup := (· ∪ ·)
  sup_le _ _ _ := union_le
  le_sup_left _ _ := le_union_left
  le_sup_right _ _ := le_union_right
  inf := (· ∩ ·)
  le_inf _ _ _ := le_inter
  inf_le_left _ _ := inter_le_left
  inf_le_right _ _ := inter_le_right
Lattice Structure on Multisets
Informal description
For any type $\alpha$, the collection of multisets over $\alpha$ forms a lattice where the meet operation is given by intersection (taking minimum multiplicities) and the join operation is given by union (taking maximum multiplicities).
Multiset.sup_eq_union theorem
(s t : Multiset α) : s ⊔ t = s ∪ t
Full source 
@[simp] lemma sup_eq_union (s t : Multiset α) : s ⊔ t = s ∪ t := rfl
Supremum Equals Union in Multiset Lattice
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the supremum (join) of $s$ and $t$ in the lattice structure on multisets is equal to their union, i.e., $s \sqcup t = s \cup t$.
Multiset.inf_eq_inter theorem
(s t : Multiset α) : s ⊓ t = s ∩ t
Full source 
@[simp] lemma inf_eq_inter (s t : Multiset α) : s ⊓ t = s ∩ t := rfl
Infimum Equals Intersection in Multiset Lattice
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the infimum (meet) of $s$ and $t$ in the lattice of multisets is equal to their intersection, i.e., $s \sqcap t = s \cap t$.
Multiset.le_inter_iff theorem
: s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u
Full source 
@[simp] lemma le_inter_iff : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u := le_inf_iff
Multiset Inclusion Order Characterization via Intersection: $s \leq t \cap u \leftrightarrow s \leq t \land s \leq u$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the inequality $s \leq t \cap u$ holds if and only if $s \leq t$ and $s \leq u$ both hold, where $\cap$ denotes the intersection of multisets (defined by taking the minimum multiplicity for each element) and $\leq$ denotes the multiset inclusion order.
Multiset.union_le_iff theorem
: s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u
Full source 
@[simp] lemma union_le_iff : s ∪ ts ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u := sup_le_iff
Union Ordering Criterion for Multisets: $s \cup t \leq u \leftrightarrow s \leq u \land t \leq u$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the union $s \cup t$ is less than or equal to $u$ if and only if both $s$ and $t$ are individually less than or equal to $u$.
Multiset.union_comm theorem
(s t : Multiset α) : s ∪ t = t ∪ s
Full source 
lemma union_comm (s t : Multiset α) : s ∪ t = t ∪ s := sup_comm ..
Commutativity of Multiset Union: $s \cup t = t \cup s$
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the union operation $\cup$ is commutative, i.e., $s \cup t = t \cup s$.
Multiset.inter_comm theorem
(s t : Multiset α) : s ∩ t = t ∩ s
Full source 
lemma inter_comm (s t : Multiset α) : s ∩ t = t ∩ s := inf_comm ..
Commutativity of Multiset Intersection
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the intersection operation is commutative, i.e., $s \cap t = t \cap s$.
Multiset.union_le_union_left theorem
(h : s ≤ t) (u) : u ∪ s ≤ u ∪ t
Full source 
@[gcongr] lemma union_le_union_left (h : s ≤ t) (u) : u ∪ s ≤ u ∪ t := sup_le_sup_left h _
Monotonicity of Union with Respect to Submultiset Order: $u \cup s \leq u \cup t$ when $s \leq t$
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then for any multiset $u$, the union $u \cup s$ is a submultiset of $u \cup t$ (i.e., $u \cup s \leq u \cup t$).
Multiset.union_le_add theorem
(s t : Multiset α) : s ∪ t ≤ s + t
Full source 
lemma union_le_add (s t : Multiset α) : s ∪ t ≤ s + t := union_le (le_add_right ..) (le_add_left ..)
Union is Submultiset of Sum: $s \cup t \leq s + t$
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the union $s \cup t$ is a submultiset of the sum $s + t$. That is, $s \cup t \leq s + t$.
Multiset.union_add_distrib theorem
(s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u)
Full source 
lemma union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u) := by
  simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using
    show s + u - (t + u) = s - t by
      rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]
Distributivity of Union over Addition in Multisets: $(s \cup t) + u = (s + u) \cup (t + u)$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the union of $s$ and $t$ followed by addition with $u$ is equal to the union of $s + u$ and $t + u$. That is, $(s \cup t) + u = (s + u) \cup (t + u)$.
Multiset.add_union_distrib theorem
(s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u)
Full source 
lemma add_union_distrib (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u) := by
  rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]
Distributivity of Addition over Union in Multisets: $s + (t \cup u) = (s + t) \cup (s + u)$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the addition of $s$ to the union of $t$ and $u$ is equal to the union of $s + t$ and $s + u$. That is, $s + (t \cup u) = (s + t) \cup (s + u)$.
Multiset.cons_union_distrib theorem
(a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
Full source 
lemma cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ sa ::ₘ s ∪ a ::ₘ t := by
  simpa using add_union_distrib (a ::ₘ 0) s t
Distributivity of Singleton Addition over Union in Multisets: $a \cup (s \cup t) = (a \cup s) \cup (a \cup t)$
Informal description
For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the multiset obtained by adding $a$ to the union of $s$ and $t$ is equal to the union of the multisets obtained by adding $a$ to $s$ and adding $a$ to $t$. That is, $a \cup (s \cup t) = (a \cup s) \cup (a \cup t)$.
Multiset.inter_add_distrib theorem
(s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u)
Full source 
lemma inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u) := by
  by_contra! h
  obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
    (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)
  rw [← cons_add] at ha
  exact (lt_cons_self (s ∩ t) a).not_le <| le_inter
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
    (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))
Distributivity of Intersection over Addition in Multisets: $(s \cap t) + u = (s + u) \cap (t + u)$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the sum of the intersection $s \cap t$ with $u$ is equal to the intersection of the sums $s + u$ and $t + u$. That is, $(s \cap t) + u = (s + u) \cap (t + u)$.
Multiset.add_inter_distrib theorem
(s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u)
Full source 
lemma add_inter_distrib (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u) := by
  rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm]
Distributivity of Addition over Intersection in Multisets: $s + (t \cap u) = (s + t) \cap (s + u)$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the sum of $s$ with the intersection $t \cap u$ is equal to the intersection of the sums $s + t$ and $s + u$. That is, $s + (t \cap u) = (s + t) \cap (s + u)$.
Multiset.cons_inter_distrib theorem
(a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)
Full source 
lemma cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t) := by
  simp
Distributivity of Multiset Addition over Intersection
Informal description
For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the multiset obtained by adding $a$ to the intersection of $s$ and $t$ is equal to the intersection of the multisets obtained by adding $a$ to $s$ and adding $a$ to $t$. That is, $a ::ₘ (s \cap t) = (a ::ₘ s) \cap (a ::ₘ t)$.
Multiset.union_add_inter theorem
(s t : Multiset α) : s ∪ t + s ∩ t = s + t
Full source 
lemma union_add_inter (s t : Multiset α) : s ∪ t + s ∩ t = s + t := by
  apply _root_.le_antisymm
  · rw [union_add_distrib]
    refine union_le (Multiset.add_le_add_left inter_le_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right inter_le_left
  · rw [Multiset.add_comm, add_inter_distrib]
    refine le_inter (Multiset.add_le_add_right le_union_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right le_union_left
Union-Intersection Addition Identity for Multisets: $(s \cup t) + (s \cap t) = s + t$
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the sum of the union $s \cup t$ and the intersection $s \cap t$ equals the sum of $s$ and $t$, i.e., $(s \cup t) + (s \cap t) = s + t$.
Multiset.sub_add_inter theorem
(s t : Multiset α) : s - t + s ∩ t = s
Full source 
lemma sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s := by
  rw [inter_comm]
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  by_cases h : a ∈ s
  · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h]
  · rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH]
Decomposition of Multiset via Difference and Intersection: $(s - t) + (s \cap t) = s$
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the sum of the difference multiset $s - t$ and the intersection multiset $s \cap t$ equals $s$. That is, $(s - t) + (s \cap t) = s$.
Multiset.sub_inter theorem
(s t : Multiset α) : s - s ∩ t = s - t
Full source 
lemma sub_inter (s t : Multiset α) : s - s ∩ t = s - t :=
  (Multiset.eq_sub_of_add_eq <| sub_add_inter ..).symm
Difference of Multiset and Intersection Equals Difference: $s - (s \cap t) = s - t$
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$, the difference between $s$ and their intersection $s \cap t$ equals the difference between $s$ and $t$, i.e., $s - (s \cap t) = s - t$.
Multiset.count_inter theorem
(a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t)
Full source 
@[simp]
lemma count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t) := by
  apply @Nat.add_left_cancel (count a (s - t))
  rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel]
Count of Element in Multiset Intersection Equals Minimum Count
Informal description
For any element $a$ of type $\alpha$ and any two multisets $s$ and $t$ over $\alpha$, the count of $a$ in the intersection $s \cap t$ is equal to the minimum of the counts of $a$ in $s$ and $t$. That is, $\text{count}_a(s \cap t) = \min(\text{count}_a(s), \text{count}_a(t))$.
Multiset.coe_inter theorem
(s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α)
Full source 
@[simp]
lemma coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α) := by ext; simp
Multiset Intersection of Lists Equals Bag Intersection
Informal description
For any two lists $s$ and $t$ of elements of type $\alpha$, the multiset intersection of $s$ and $t$ is equal to the bag intersection (multiset intersection) of $s$ and $t$ when viewed as lists. That is, $(s \cap t : \text{Multiset } \alpha) = (s.\text{bagInter } t : \text{List } \alpha)$.
Multiset.instDistribLattice instance
: DistribLattice (Multiset α)
Full source 
instance instDistribLattice : DistribLattice (Multiset α) where
  le_sup_inf s t u := ge_of_eq <| ext.2 fun a ↦ by
    simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union,
      Multiset.count_union, Multiset.inf_eq_inter]
Distributive Lattice Structure on Multisets
Informal description
For any type $\alpha$, the collection of multisets over $\alpha$ forms a distributive lattice where the meet operation is given by intersection (taking minimum multiplicities) and the join operation is given by union (taking maximum multiplicities).
Multiset.filter_inter theorem
(p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s ∩ t) = filter p s ∩ filter p t
Full source 
@[simp] lemma filter_inter (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
    filter p (s ∩ t) = filterfilter p s ∩ filter p t :=
  le_antisymm (le_inter (filter_le_filter _ inter_le_left) (filter_le_filter _ inter_le_right)) <|
    le_filter.2 ⟨inf_le_inf (filter_le _ _) (filter_le _ _), fun _a h =>
      of_mem_filter (mem_of_le inter_le_left h)⟩
Filtering Preserves Multiset Intersection
Informal description
For any predicate \( p \) on elements of type \( \alpha \) (with a decidable instance), and for any multisets \( s \) and \( t \) over \( \alpha \), the filtered multiset of the intersection \( s \cap t \) with respect to \( p \) is equal to the intersection of the filtered multisets \( \mathrm{filter}\, p\, s \) and \( \mathrm{filter}\, p\, t \). In symbols: \[ \mathrm{filter}\, p\, (s \cap t) = \mathrm{filter}\, p\, s \cap \mathrm{filter}\, p\, t. \]
Multiset.replicate_inter theorem
(n : ℕ) (x : α) (s : Multiset α) : replicate n x ∩ s = replicate (min n (s.count x)) x
Full source 
@[simp]
theorem replicate_inter (n : ℕ) (x : α) (s : Multiset α) :
    replicatereplicate n x ∩ s = replicate (min n (s.count x)) x := by
  ext y
  rw [count_inter, count_replicate, count_replicate]
  by_cases h : x = y
  · simp only [h, if_true]
  · simp only [h, if_false, Nat.zero_min]
Intersection of Replicated Multiset with Another Multiset
Informal description
For any natural number $n$, any element $x$ of type $\alpha$, and any multiset $s$ over $\alpha$, the intersection of the multiset consisting of $n$ copies of $x$ with $s$ is equal to the multiset consisting of $\min(n, \text{count}_x(s))$ copies of $x$. That is, \[ \text{replicate}_n(x) \cap s = \text{replicate}_{\min(n, \text{count}_x(s))}(x). \]
Multiset.inter_replicate theorem
(s : Multiset α) (n : ℕ) (x : α) : s ∩ replicate n x = replicate (min (s.count x) n) x
Full source 
@[simp]
theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) :
    s ∩ replicate n x = replicate (min (s.count x) n) x := by
  rw [inter_comm, replicate_inter, min_comm]
Intersection of Multiset with Replicated Element Yields Minimum Count
Informal description
For any multiset $s$ over a type $\alpha$, any natural number $n$, and any element $x \in \alpha$, the intersection of $s$ with the multiset consisting of $n$ copies of $x$ is equal to the multiset consisting of $\min(\text{count}_x(s), n)$ copies of $x$. That is, \[ s \cap \text{replicate}_n(x) = \text{replicate}_{\min(\text{count}_x(s), n)}(x). \]
Multiset.inter_add_sub_of_add_eq_add theorem
[DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) : (N ∩ Q) + (P - M) = N
Full source 
theorem inter_add_sub_of_add_eq_add [DecidableEq α] {M N P Q : Multiset α} (h : M + N = P + Q) :
    (N ∩ Q) + (P - M) = N := by
  ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.mem_add, Multiset.count_add]
  omega
Intersection and Difference Identity for Multiset Addition
Informal description
For any type $\alpha$ with decidable equality and any multisets $M, N, P, Q$ over $\alpha$ such that $M + N = P + Q$, we have $(N \cap Q) + (P - M) = N$.
Multiset.Disjoint definition
(s t : Multiset α) : Prop
Full source 
/-- `Disjoint s t` means that `s` and `t` have no elements in common. -/
@[deprecated _root_.Disjoint (since := "2024-11-01")]
protected def Disjoint (s t : Multiset α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → a ∈ t → False
Disjoint multisets
Informal description
Two multisets $s$ and $t$ are called *disjoint* if they have no common elements, i.e., for any element $a$, if $a$ belongs to $s$ then it does not belong to $t$, and vice versa.
Multiset.disjoint_left theorem
{s t : Multiset α} : Disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t
Full source 
theorem disjoint_left {s t : Multiset α} : DisjointDisjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t := by
  refine ⟨fun h a hs ht ↦ ?_, fun h u hs ht ↦ ?_⟩
  · simpa using h (singleton_le.mpr hs) (singleton_le.mpr ht)
  · rw [le_bot_iff, bot_eq_zero, eq_zero_iff_forall_not_mem]
    exact fun a ha ↦ h (subset_of_le hs ha) (subset_of_le ht ha)
Characterization of Disjoint Multisets via Left Inclusion
Informal description
Two multisets $s$ and $t$ are disjoint if and only if for every element $a$, if $a$ belongs to $s$ then $a$ does not belong to $t$.
Multiset.coe_disjoint theorem
(l₁ l₂ : List α) : Disjoint (l₁ : Multiset α) l₂ ↔ l₁.Disjoint l₂
Full source 
@[simp, norm_cast]
theorem coe_disjoint (l₁ l₂ : List α) : DisjointDisjoint (l₁ : Multiset α) l₂ ↔ l₁.Disjoint l₂ :=
  disjoint_left
Disjointness of Multiset from List vs. List Disjointness
Informal description
For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the multiset obtained from $l₁$ is disjoint from $l₂$ if and only if the lists $l₁$ and $l₂$ are disjoint as lists. Here, two lists are disjoint if they have no common elements.
Multiset.disjoint_of_subset_left theorem
{s t u : Multiset α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t
Full source 
theorem disjoint_of_subset_left {s t u : Multiset α} (h : s ⊆ u) (d : Disjoint u t) :
    Disjoint s t :=
  disjoint_left.mpr fun ha ↦ disjoint_left.mp d <| h ha
Disjointness Preservation under Left Subset Inclusion for Multisets
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, if $s$ is a subset of $u$ and $u$ is disjoint from $t$, then $s$ is disjoint from $t$.
Multiset.disjoint_of_subset_right theorem
{s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t
Full source 
theorem disjoint_of_subset_right {s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) :
    Disjoint s t :=
  (disjoint_of_subset_left h d.symm).symm
Disjointness Preservation under Right Subset Inclusion for Multisets
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, if $t$ is a subset of $u$ and $s$ is disjoint from $u$, then $s$ is disjoint from $t$.
Multiset.zero_disjoint theorem
(l : Multiset α) : Disjoint 0 l
Full source 
@[simp]
theorem zero_disjoint (l : Multiset α) : Disjoint 0 l := disjoint_bot_left
Empty multiset is disjoint from any multiset
Informal description
For any multiset $l$ over a type $\alpha$, the empty multiset $0$ is disjoint from $l$.
Multiset.singleton_disjoint theorem
{l : Multiset α} {a : α} : Disjoint { a } l ↔ a ∉ l
Full source 
@[simp]
theorem singleton_disjoint {l : Multiset α} {a : α} : DisjointDisjoint {a} l ↔ a ∉ l := by
  simp [disjoint_left]
Disjointness of Singleton Multiset: $\{a\} \perp l \leftrightarrow a \notin l$
Informal description
For any multiset $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the singleton multiset $\{a\}$ is disjoint from $l$ if and only if $a$ does not belong to $l$ (i.e., $a \notin l$).
Multiset.disjoint_singleton theorem
{l : Multiset α} {a : α} : Disjoint l { a } ↔ a ∉ l
Full source 
@[simp]
theorem disjoint_singleton {l : Multiset α} {a : α} : DisjointDisjoint l {a} ↔ a ∉ l := by
  rw [_root_.disjoint_comm, singleton_disjoint]
Disjointness of Multiset with Singleton: $l \perp \{a\} \leftrightarrow a \notin l$
Informal description
For any multiset $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the multiset $l$ is disjoint from the singleton multiset $\{a\}$ if and only if $a$ does not belong to $l$ (i.e., $a \notin l$).
Multiset.disjoint_add_left theorem
{s t u : Multiset α} : Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u
Full source 
@[simp]
theorem disjoint_add_left {s t u : Multiset α} :
    DisjointDisjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u := by simp [disjoint_left, or_imp, forall_and]
Disjointness of Multiset Sum on the Left
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the sum $s + t$ is disjoint from $u$ if and only if both $s$ is disjoint from $u$ and $t$ is disjoint from $u$. In other words, $s + t \mathbin{\#} u \leftrightarrow s \mathbin{\#} u \land t \mathbin{\#} u$, where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_add_right theorem
{s t u : Multiset α} : Disjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u
Full source 
@[simp]
theorem disjoint_add_right {s t u : Multiset α} :
    DisjointDisjoint s (t + u) ↔ Disjoint s t ∧ Disjoint s u := by
  rw [_root_.disjoint_comm, disjoint_add_left]; tauto
Disjointness of Multiset Sum on the Right
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$, the multiset $s$ is disjoint from the sum $t + u$ if and only if $s$ is disjoint from both $t$ and $u$. In other words, $s \mathbin{\#} (t + u) \leftrightarrow s \mathbin{\#} t \land s \mathbin{\#} u$, where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_cons_left theorem
{a : α} {s t : Multiset α} : Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t
Full source 
@[simp]
theorem disjoint_cons_left {a : α} {s t : Multiset α} :
    DisjointDisjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t :=
  (@disjoint_add_left _ {a} s t).trans <| by rw [singleton_disjoint]
Disjointness of Prepended Multiset: $\{a\} \cup s \perp t \leftrightarrow a \notin t \land s \perp t$
Informal description
For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiset obtained by prepending $a$ to $s$ (denoted $a ::ₘ s$) is disjoint from $t$ if and only if $a$ does not belong to $t$ and $s$ is disjoint from $t$. In symbols: $$ \{a\} \cup s \mathbin{\#} t \leftrightarrow a \notin t \land s \mathbin{\#} t $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_cons_right theorem
{a : α} {s t : Multiset α} : Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t
Full source 
@[simp]
theorem disjoint_cons_right {a : α} {s t : Multiset α} :
    DisjointDisjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t := by
  rw [_root_.disjoint_comm, disjoint_cons_left]; tauto
Disjointness of Prepended Multiset on the Right: $s \perp \{a\} \cup t \leftrightarrow a \notin s \land s \perp t$
Informal description
For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, the multiset $s$ is disjoint from the multiset obtained by prepending $a$ to $t$ (denoted $a ::ₘ t$) if and only if $a$ does not belong to $s$ and $s$ is disjoint from $t$. In symbols: $$ s \mathbin{\#} (\{a\} \cup t) \leftrightarrow a \notin s \land s \mathbin{\#} t $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.inter_eq_zero_iff_disjoint theorem
[DecidableEq α] {s t : Multiset α} : s ∩ t = 0 ↔ Disjoint s t
Full source 
theorem inter_eq_zero_iff_disjoint [DecidableEq α] {s t : Multiset α} :
    s ∩ ts ∩ t = 0 ↔ Disjoint s t := by rw [← subset_zero]; simp [subset_iff, disjoint_left]
Intersection Equals Zero if and only if Disjoint Multisets
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$ with decidable equality, the intersection $s \cap t$ is the empty multiset if and only if $s$ and $t$ are disjoint. In symbols: $$ s \cap t = 0 \leftrightarrow s \mathbin{\#} t $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_union_left theorem
[DecidableEq α] {s t u : Multiset α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
Full source 
@[simp]
theorem disjoint_union_left [DecidableEq α] {s t u : Multiset α} :
    DisjointDisjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u :=  disjoint_sup_left
Disjointness of Union on the Left: $(s \cup t) \mathbin{\#} u \leftrightarrow s \mathbin{\#} u \land t \mathbin{\#} u$
Informal description
For any multisets $s$, $t$, and $u$ over a type $\alpha$ with decidable equality, the union $s \cup t$ is disjoint from $u$ if and only if both $s$ and $t$ are disjoint from $u$ individually. In symbols: $$ (s \cup t) \mathbin{\#} u \leftrightarrow s \mathbin{\#} u \land t \mathbin{\#} u $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_union_right theorem
[DecidableEq α] {s t u : Multiset α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
Full source 
@[simp]
theorem disjoint_union_right [DecidableEq α] {s t u : Multiset α} :
    DisjointDisjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u := disjoint_sup_right
Disjointness with Union of Multisets
Informal description
For any three multisets $s$, $t$, and $u$ over a type $\alpha$ with decidable equality, the multiset $s$ is disjoint from the union $t \cup u$ if and only if $s$ is disjoint from both $t$ and $u$. In symbols: $$ s \mathbin{\#} (t \cup u) \leftrightarrow s \mathbin{\#} t \text{ and } s \mathbin{\#} u $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.add_eq_union_iff_disjoint theorem
[DecidableEq α] {s t : Multiset α} : s + t = s ∪ t ↔ Disjoint s t
Full source 
theorem add_eq_union_iff_disjoint [DecidableEq α] {s t : Multiset α} :
    s + t = s ∪ t ↔ Disjoint s t := by
  simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
    Nat.min_eq_zero_iff, Nat.add_eq_max_iff]
Sum Equals Union if and only if Disjoint Multisets
Informal description
For any two multisets $s$ and $t$ over a type $\alpha$ with decidable equality, the sum $s + t$ equals the union $s \cup t$ if and only if $s$ and $t$ are disjoint. In symbols: $$ s + t = s \cup t \leftrightarrow s \mathbin{\#} t $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.add_eq_union_left_of_le theorem
[DecidableEq α] {s t u : Multiset α} (h : t ≤ s) : u + s = u ∪ t ↔ Disjoint u s ∧ s = t
Full source 
lemma add_eq_union_left_of_le [DecidableEq α] {s t u : Multiset α} (h : t ≤ s) :
    u + s = u ∪ t ↔ Disjoint u s ∧ s = t := by
  rw [← add_eq_union_iff_disjoint]
  refine ⟨fun h0 ↦ ?_, ?_⟩
  · rw [and_iff_right_of_imp]
    · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h
    · rintro rfl
      exact h0
  · rintro ⟨h0, rfl⟩
    exact h0
Sum Equals Union Under Submultiset Condition: $u + s = u \cup t \leftrightarrow u \mathbin{\#} s \text{ and } s = t$
Informal description
For any three multisets $s$, $t$, and $u$ over a type $\alpha$ with decidable equality, if $t$ is a submultiset of $s$ (i.e., $t \leq s$), then the sum $u + s$ equals the union $u \cup t$ if and only if $u$ and $s$ are disjoint and $s = t$. In symbols: $$ u + s = u \cup t \leftrightarrow u \mathbin{\#} s \text{ and } s = t $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.add_eq_union_right_of_le theorem
[DecidableEq α] {x y z : Multiset α} (h : z ≤ y) : x + y = x ∪ z ↔ y = z ∧ Disjoint x y
Full source 
lemma add_eq_union_right_of_le [DecidableEq α] {x y z : Multiset α} (h : z ≤ y) :
    x + y = x ∪ z ↔ y = z ∧ Disjoint x y := by
  simpa only [and_comm] using add_eq_union_left_of_le h
Sum Equals Union Under Submultiset Condition (Right Version): $x + y = x \cup z \leftrightarrow y = z \text{ and } x \mathbin{\#} y$
Informal description
For any three multisets $x$, $y$, and $z$ over a type $\alpha$ with decidable equality, if $z$ is a submultiset of $y$ (i.e., $z \leq y$), then the sum $x + y$ equals the union $x \cup z$ if and only if $y = z$ and $x$ and $y$ are disjoint. In symbols: $$ x + y = x \cup z \leftrightarrow y = z \text{ and } x \mathbin{\#} y $$ where $\mathbin{\#}$ denotes the disjointness relation.
Multiset.disjoint_map_map theorem
{f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} : Disjoint (s.map f) (t.map g) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b
Full source 
theorem disjoint_map_map {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} :
    DisjointDisjoint (s.map f) (t.map g) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b := by
  simp [disjoint_iff_ne]
Disjointness of Mapped Multisets via Function Images
Informal description
For any functions $f : \alpha \to \gamma$ and $g : \beta \to \gamma$, and any multisets $s$ over $\alpha$ and $t$ over $\beta$, the mapped multisets $s.map\, f$ and $t.map\, g$ are disjoint if and only if for every element $a \in s$ and every element $b \in t$, the images $f(a)$ and $g(b)$ are distinct. In symbols: \[ \text{Disjoint}\, (s.map\, f)\, (t.map\, g) \leftrightarrow \forall a \in s, \forall b \in t, f(a) \neq g(b). \]
Multiset.map_set_pairwise theorem
{f : α → β} {r : β → β → Prop} {m : Multiset α} (h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) : {b | b ∈ m.map f}.Pairwise r
Full source 
theorem map_set_pairwise {f : α → β} {r : β → β → Prop} {m : Multiset α}
    (h : { a | a ∈ m }.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) : { b | b ∈ m.map f }.Pairwise r :=
  fun b₁ h₁ b₂ h₂ hn => by
    obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
    exact h H₁ H₂ (mt (congr_arg f) hn)
Pairwise Relation Preservation under Multiset Mapping
Informal description
Let $f : \alpha \to \beta$ be a function, $r : \beta \to \beta \to \mathrm{Prop}$ a relation, and $m$ a multiset over $\alpha$. If the set $\{a \mid a \in m\}$ is pairwise related via $\lambda a_1 a_2, r (f a_1) (f a_2)$, then the set $\{b \mid b \in \mathrm{map}\, f\, m\}$ is pairwise related via $r$.
Multiset.nodup_add theorem
{s t : Multiset α} : Nodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t
Full source 
theorem nodup_add {s t : Multiset α} : NodupNodup (s + t) ↔ Nodup s ∧ Nodup t ∧ Disjoint s t :=
  Quotient.inductionOn₂ s t fun _ _ => by simp [nodup_append]
No-Duplicates Condition for Multiset Sum: $Nodup(s + t) \leftrightarrow Nodup(s) \land Nodup(t) \land Disjoint(s, t)$
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, the sum $s + t$ has no duplicate elements if and only if $s$ has no duplicates, $t$ has no duplicates, and $s$ and $t$ are disjoint (i.e., they share no common elements).
Multiset.disjoint_of_nodup_add theorem
{s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t
Full source 
theorem disjoint_of_nodup_add {s t : Multiset α} (d : Nodup (s + t)) : Disjoint s t :=
  (nodup_add.1 d).2.2
Disjointness from No-Duplicates Sum Condition: $Nodup(s + t) \implies Disjoint(s, t)$
Informal description
For any multisets $s$ and $t$ over a type $\alpha$, if the sum $s + t$ has no duplicate elements, then $s$ and $t$ are disjoint (i.e., they share no common elements).
Multiset.Nodup.add_iff theorem
(d₁ : Nodup s) (d₂ : Nodup t) : Nodup (s + t) ↔ Disjoint s t
Full source 
theorem Nodup.add_iff (d₁ : Nodup s) (d₂ : Nodup t) : NodupNodup (s + t) ↔ Disjoint s t := by
  simp [nodup_add, d₁, d₂]
Nodup of Sum of Multisets is Equivalent to Disjointness
Informal description
For any two multisets $s$ and $t$ with no duplicate elements (i.e., `Nodup s` and `Nodup t`), the sum $s + t$ has no duplicate elements if and only if $s$ and $t$ are disjoint (i.e., `Disjoint s t`).
Multiset.Nodup.inter_left theorem
[DecidableEq α] (t) : Nodup s → Nodup (s ∩ t)
Full source 
lemma Nodup.inter_left [DecidableEq α] (t) : Nodup s → Nodup (s ∩ t) := nodup_of_le inter_le_left
Preservation of No-Duplicates Property under Left Intersection
Informal description
For any type $\alpha$ with decidable equality and any multiset $t$ over $\alpha$, if a multiset $s$ has no duplicate elements (i.e., $\text{Nodup}(s)$), then the intersection $s \cap t$ also has no duplicate elements (i.e., $\text{Nodup}(s \cap t)$).
Multiset.Nodup.inter_right theorem
[DecidableEq α] (s) : Nodup t → Nodup (s ∩ t)
Full source 
lemma Nodup.inter_right [DecidableEq α] (s) : Nodup t → Nodup (s ∩ t) := nodup_of_le inter_le_right
Preservation of No-Duplicates Property under Right Intersection
Informal description
For any type $\alpha$ with decidable equality and any multiset $s$ over $\alpha$, if a multiset $t$ has no duplicate elements (i.e., $\text{Nodup}(t)$), then the intersection $s \cap t$ also has no duplicate elements (i.e., $\text{Nodup}(s \cap t)$).
Multiset.nodup_union theorem
[DecidableEq α] {s t : Multiset α} : Nodup (s ∪ t) ↔ Nodup s ∧ Nodup t
Full source 
@[simp]
theorem nodup_union [DecidableEq α] {s t : Multiset α} : NodupNodup (s ∪ t) ↔ Nodup s ∧ Nodup t :=
  ⟨fun h => ⟨nodup_of_le le_union_left h, nodup_of_le le_union_right h⟩, fun ⟨h₁, h₂⟩ =>
    nodup_iff_count_le_one.2 fun a => by
      rw [count_union]
      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)⟩
Union of Multisets is Nodup if and only if Both Multisets are Nodup
Informal description
For any multisets $s$ and $t$ over a type $\alpha$ with decidable equality, the union $s \cup t$ has no duplicate elements if and only if both $s$ and $t$ individually have no duplicate elements. In other words: $$\text{Nodup}(s \cup t) \leftrightarrow \text{Nodup}(s) \land \text{Nodup}(t).$$