# Multisets #

Multisets are finite sets with duplicates allowed. They are implemented here as the quotient of lists by permutation. This gives them computational content.

This file contains the definition of `Multiset` and the basic predicates. Most operations have been split off into their own files. The goal is that we can define `Finset` with only importing `Multiset.Defs`.

## Main definitions #

- `Multiset`: the type of finite sets with duplicates allowed.

- `Coe (List α) (Multiset α)`: turn a list into a multiset by forgetting the order.

- `Multiset.pmap`: map a partial function defined on a superset of the multiset's elements.

- `Multiset.attach`: add a proof of membership to the elements of the multiset.

- `Multiset.card`: number of elements of a multiset (counted with repetition).

- `Membership α (Multiset α)` instance: `x ∈ s` if `x` has multiplicity at least one in `s`.

- `Subset (Multiset α)` instance: `s ⊆ t` if every `x ∈ s` also enjoys `x ∈ t`.

- `PartialOrder (Multiset α)` instance: `s ≤ t` if all `x` have multiplicity in `s` less than their multiplicity in `t`.

- `Multiset.Pairwise`: `Pairwise r s` holds iff there exists a list of elements of `s` such that `r` holds pairwise.

- `Multiset.Nodup`: `Nodup s` holds if the multiplicity of any element is at most 1.

## Notation (defined later) #

- `0`: The empty multiset.
- `{a}`: The multiset containing a single occurrence of `a`.
- `a ::ₘ s`: The multiset containing one more occurrence of `a` than `s` does.
- `s + t`: The multiset for which the number of occurrences of each `a` is the sum of the occurrences of `a` in `s` and `t`.
- `s - t`: The multiset for which the number of occurrences of each `a` is the difference of the occurrences of `a` in `s` and `t`.
- `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`.

source
def Multiset (α : Type u) :
Type u

`Multiset α` is the quotient of `List α` by list permutation. The result is a type of finite sets with duplicates allowed.

Equations

- Multiset α = Quotient (List.isSetoid α)

Instances For

source
def Multiset.ofList {α : Type u_1} :
List α → Multiset α

The quotient map from `List α` to `Multiset α`.

Equations

- Multiset.ofList = Quot.mk ⇑(List.isSetoid α)

Instances For

source
instance Multiset.instCoeList {α : Type u_1} :
Coe (List α) (Multiset α)
Equations

- Multiset.instCoeList = { coe := Multiset.ofList }

source
@[simp]
theorem Multiset.quot_mk_to_coe {α : Type u_1} (l : List α) :
⟦l⟧ = ↑l
source
@[simp]
theorem Multiset.quot_mk_to_coe' {α : Type u_1} (l : List α) :
Quot.mk (fun (x1 x2 : List α) => x1 ≈ x2) l = ↑l
source
@[simp]
theorem Multiset.quot_mk_to_coe'' {α : Type u_1} (l : List α) :
Quot.mk (⇑(List.isSetoid α)) l = ↑l
source
@[simp]
theorem Multiset.lift_coe {α : Type u_3} {β : Type u_4} (x : List α) (f : List α → β) (h : ∀ (a b : List α), a ≈ b → f a = f b) :
Quotient.lift f h ↑x = f x
source
@[simp]
theorem Multiset.coe_eq_coe {α : Type u_1} {l₁ l₂ : List α} :
↑l₁ = ↑l₂ ↔ l₁.Perm l₂
source
instance Multiset.instDecidableEquivListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
Decidable (l₁ ≈ l₂)
Equations

- Multiset.instDecidableEquivListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

source
instance Multiset.instDecidableRListOfDecidableEq {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) :
Decidable ((List.isSetoid α) l₁ l₂)
Equations

- Multiset.instDecidableRListOfDecidableEq l₁ l₂ = inferInstanceAs (Decidable (l₁.Perm l₂))

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

- x✝¹.decidableEq x✝ = Quotient.recOnSubsingleton₂ x✝¹ x✝ fun (x x_1 : List α) => decidable_of_iff' (x ≈ x_1) ⋯

source
def Multiset.Mem {α : Type u_1} (s : Multiset α) (a : α) :
Prop

`a ∈ s` means that `a` has nonzero multiplicity in `s`.

Equations

- s.Mem a = Quot.liftOn s (fun (l : List α) => a ∈ l) ⋯

Instances For

source
instance Multiset.instMembership {α : Type u_1} :
Membership α (Multiset α)
Equations

- Multiset.instMembership = { mem := Multiset.Mem }

source
@[simp]
theorem Multiset.mem_coe {α : Type u_1} {a : α} {l : List α} :
a ∈ ↑l ↔ a ∈ l
source
instance Multiset.decidableMem {α : Type u_1} [DecidableEq α] (a : α) (s : Multiset α) :
Decidable (a ∈ s)
Equations

- Multiset.decidableMem a s = Quot.recOnSubsingleton s fun (l : List α) => inferInstanceAs (Decidable (a ∈ l))

### `Multiset.Subset` #

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

`s ⊆ t` is the lift of the list subset relation. It means that any element with nonzero multiplicity in `s` has nonzero multiplicity in `t`, but it does not imply that the multiplicity of `a` in `s` is less or equal than in `t`; see `s ≤ t` for this relation.

Equations

- s.Subset t = ∀ ⦃a : α⦄, a ∈ s → a ∈ t

Instances For

source
instance Multiset.instHasSubset {α : Type u_1} :
HasSubset (Multiset α)
Equations

- Multiset.instHasSubset = { Subset := Multiset.Subset }

source
instance Multiset.instHasSSubset {α : Type u_1} :
HasSSubset (Multiset α)
Equations

- Multiset.instHasSSubset = { SSubset := fun (s t : Multiset α) => s ⊆ t ∧ ¬t ⊆ s }

source
instance Multiset.instIsNonstrictStrictOrder {α : Type u_1} :
IsNonstrictStrictOrder (Multiset α) (fun (x1 x2 : Multiset α) => x1 ⊆ x2) fun (x1 x2 : Multiset α) => x1 ⊂ x2
source
@[simp]
theorem Multiset.coe_subset {α : Type u_1} {l₁ l₂ : List α} :
↑l₁ ⊆ ↑l₂ ↔ l₁ ⊆ l₂
source
@[simp]
theorem Multiset.Subset.refl {α : Type u_1} (s : Multiset α) :
s ⊆ s
source
theorem Multiset.Subset.trans {α : Type u_1} {s t u : Multiset α} :
s ⊆ t → t ⊆ u → s ⊆ u
source
theorem Multiset.subset_iff {α : Type u_1} {s t : Multiset α} :
s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t
source
theorem Multiset.mem_of_subset {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) :
a ∈ s → a ∈ t

### Partial order on `Multiset`s #

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

`s ≤ t` means that `s` is a sublist of `t` (up to permutation). Equivalently, `s ≤ t` means that `count a s ≤ count a t` for all `a`.

Equations

- s.Le t = Quotient.liftOn₂ s t (fun (x1 x2 : List α) => x1.Subperm x2) ⋯

Instances For

source
instance Multiset.instPartialOrder {α : Type u_1} :
PartialOrder (Multiset α)
Equations

- Multiset.instPartialOrder = { le := Multiset.Le, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

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

- s.decidableLE t = Quotient.recOnSubsingleton₂ s t List.decidableSubperm

source
theorem Multiset.subset_of_le {α : Type u_1} {s t : Multiset α} :
s ≤ t → s ⊆ t
source
theorem Multiset.Le.subset {α : Type u_1} {s t : Multiset α} :
s ≤ t → s ⊆ t

Alias of `Multiset.subset_of_le`.

source
theorem Multiset.mem_of_le {α : Type u_1} {s t : Multiset α} {a : α} (h : s ≤ t) :
a ∈ s → a ∈ t
source
theorem Multiset.notMem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) :
¬a ∈ t → ¬a ∈ s
source
@[deprecated Multiset.notMem_mono (since := "2025-05-23")]
theorem Multiset.not_mem_mono {α : Type u_1} {s t : Multiset α} {a : α} (h : s ⊆ t) :
¬a ∈ t → ¬a ∈ s

Alias of `Multiset.notMem_mono`.

source
@[simp]
theorem Multiset.coe_le {α : Type u_1} {l₁ l₂ : List α} :
↑l₁ ≤ ↑l₂ ↔ l₁.Subperm l₂
source
theorem Multiset.leInductionOn {α : Type u_1} {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t) (H : ∀ {l₁ l₂ : List α}, l₁.Sublist l₂ → C ↑l₁ ↑l₂) :
C s t

### Cardinality #

source
def Multiset.card {α : Type u_1} :
Multiset α → ℕ

The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list.

Equations

- Multiset.card = Quot.lift List.length ⋯

Instances For

source
@[simp]
theorem Multiset.coe_card {α : Type u_1} (l : List α) :
(↑l).card = l.length
source
theorem Multiset.card_le_card {α : Type u_1} {s t : Multiset α} (h : s ≤ t) :
s.card ≤ t.card
source
theorem Multiset.eq_of_le_of_card_le {α : Type u_1} {s t : Multiset α} (h : s ≤ t) :
t.card ≤ s.card → s = t
source
theorem Multiset.card_lt_card {α : Type u_1} {s t : Multiset α} (h : s < t) :
s.card < t.card
source
theorem Multiset.card_mono {α : Type u_1} :
Monotone card
source
theorem Multiset.card_strictMono {α : Type u_1} :
StrictMono card
source
instance Multiset.instWellFoundedLT {α : Type u_1} :
WellFoundedLT (Multiset α)

Another way of expressing `strongInductionOn`: the `(<)` relation is well-founded.

source
@[simp]
theorem Multiset.coe_reverse {α : Type u_1} (l : List α) :
↑l.reverse = ↑l

### Map for partial functions #

source
def Multiset.pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) :
(∀ (a : α), a ∈ s → p a) → Multiset β

Lift of the list `pmap` operation. Map a partial function `f` over a multiset `s` whose elements are all in the domain of `f`.

Equations

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

Instances For

source
@[simp]
theorem Multiset.coe_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (l : List α) (H : ∀ (a : α), a ∈ l → p a) :
pmap f (↑l) H = ↑(List.pmap f l H)
source
theorem Multiset.pmap_congr {α : Type u_1} {β : Type v} {p q : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → q a → β} (s : Multiset α) {H₁ : ∀ (a : α), a ∈ s → p a} {H₂ : ∀ (a : α), a ∈ s → q a} :
(∀ (a : α), a ∈ s → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂
source
@[simp]
theorem Multiset.mem_pmap {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ (a : α), a ∈ s → p a} {b : β} :
b ∈ pmap f s H ↔ ∃ (a : α), ∃ (h : a ∈ s), f a ⋯ = b
source
@[simp]
theorem Multiset.card_pmap {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ (a : α), a ∈ s → p a) :
(pmap f s H).card = s.card
source
def Multiset.attach {α : Type u_1} (s : Multiset α) :
Multiset { x : α // x ∈ s }

"Attach" a proof that `a ∈ s` to each element `a` in `s` to produce a multiset on `{x // x ∈ s}`.

Equations

- s.attach = Multiset.pmap Subtype.mk s ⋯

Instances For

source
@[simp]
theorem Multiset.coe_attach {α : Type u_1} (l : List α) :
(↑l).attach = ↑l.attach
source
@[simp]
theorem Multiset.mem_attach {α : Type u_1} (s : Multiset α) (x : { x : α // x ∈ s }) :
x ∈ s.attach
source
@[simp]
theorem Multiset.card_attach {α : Type u_1} {m : Multiset α} :
m.attach.card = m.card
source
def Multiset.decidableForallMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [(a : α) → Decidable (p a)] :
Decidable (∀ (a : α), a ∈ m → p a)

If `p` is a decidable predicate, so is the predicate that all elements of a multiset satisfy `p`.

Equations

- Multiset.decidableForallMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∀ (a : α), a ∈ l → p a) ⋯

Instances For

source
instance Multiset.decidableDforallMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] :
Decidable (∀ (a : α) (h : a ∈ m), p a h)
Equations

- Multiset.decidableDforallMultiset = decidable_of_iff (∀ (a : { x : α // x ∈ m }), a ∈ m.attach → p ↑a ⋯) ⋯

source
instance Multiset.decidableEqPiMultiset {α : Type u_1} {m : Multiset α} {β : α → Type u_3} [(a : α) → DecidableEq (β a)] :
DecidableEq ((a : α) → a ∈ m → β a)

decidable equality for functions whose domain is bounded by multisets

Equations

- Multiset.decidableEqPiMultiset f g = decidable_of_iff (∀ (a : α) (h : a ∈ m), f a h = g a h) ⋯

source
def Multiset.decidableExistsMultiset {α : Type u_1} {m : Multiset α} {p : α → Prop} [DecidablePred p] :
Decidable (∃ (x : α), x ∈ m ∧ p x)

If `p` is a decidable predicate, so is the existence of an element in a multiset satisfying `p`.

Equations

- Multiset.decidableExistsMultiset = Quotient.recOnSubsingleton m fun (l : List α) => decidable_of_iff (∃ (a : α), a ∈ l ∧ p a) ⋯

Instances For

source
instance Multiset.decidableDexistsMultiset {α : Type u_1} {m : Multiset α} {p : (a : α) → a ∈ m → Prop} [_hp : (a : α) → (h : a ∈ m) → Decidable (p a h)] :
Decidable (∃ (a : α), ∃ (h : a ∈ m), p a h)
Equations

- Multiset.decidableDexistsMultiset = decidable_of_iff (∃ (x : { a : α // a ∈ m }), x ∈ m.attach ∧ p ↑x ⋯) ⋯

source
def Multiset.Pairwise {α : Type u_1} (r : α → α → Prop) (m : Multiset α) :
Prop

`Pairwise r m` states that there exists a list of the elements s.t. `r` holds pairwise on this list.

Equations

- Multiset.Pairwise r m = ∃ (l : List α), m = ↑l ∧ List.Pairwise r l

Instances For

source
theorem Multiset.pairwise_coe_iff {α : Type u_1} {r : α → α → Prop} {l : List α} :
Pairwise r ↑l ↔ ∃ (l' : List α), l.Perm l' ∧ List.Pairwise r l'
source
theorem Multiset.pairwise_coe_iff_pairwise {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) {l : List α} :
Pairwise r ↑l ↔ List.Pairwise r l
source
def Multiset.Nodup {α : Type u_1} (s : Multiset α) :
Prop

`Nodup s` means that `s` has no duplicates, i.e. the multiplicity of any element is at most 1.

Equations

- s.Nodup = Quot.liftOn s List.Nodup ⋯

Instances For

source
@[simp]
theorem Multiset.coe_nodup {α : Type u_1} {l : List α} :
(↑l).Nodup ↔ l.Nodup
source
theorem Multiset.Nodup.ext {α : Type u_1} {s t : Multiset α} :
s.Nodup → t.Nodup → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)
source
theorem Multiset.le_iff_subset {α : Type u_1} {s t : Multiset α} :
s.Nodup → (s ≤ t ↔ s ⊆ t)
source
theorem Multiset.nodup_of_le {α : Type u_1} {s t : Multiset α} (h : s ≤ t) :
t.Nodup → s.Nodup
source
instance Multiset.nodupDecidable {α : Type u_1} [DecidableEq α] (s : Multiset α) :
Decidable s.Nodup
Equations

- s.nodupDecidable = Quotient.recOnSubsingleton s fun (l : List α) => l.nodupDecidable

source
def Multiset.sizeOf {α : Type u_1} [SizeOf α] (s : Multiset α) :
ℕ

Defines a size for a multiset by referring to the size of the underlying list.

This has to be defined before the definition of `Finset`, otherwise its automatically generated `SizeOf` instance will be wrong.

Equations

- s.sizeOf = Quot.liftOn s sizeOf ⋯

Instances For

source
instance Multiset.instSizeOf {α : Type u_1} [SizeOf α] :
SizeOf (Multiset α)
Equations

- Multiset.instSizeOf = { sizeOf := Multiset.sizeOf }