Mathlib.Data.Multiset.Defs

Module docstring

{"# 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. ","### Multiset.Subset ","### Partial order on Multisets ","### Cardinality ","### Map for partial functions "}

Multiset definition

(α : Type u) : Type u

Full source

/-- `Multiset α` is the quotient of `List α` by list permutation. The result
  is a type of finite sets with duplicates allowed. -/
def Multiset.{u} (α : Type u) : Type u :=
  Quotient (List.isSetoid α)

Multiset (finite bag with duplicates)

Informal description

The type `Multiset α` represents finite multisets (bags) over a type `α`, where elements can appear multiple times. It is defined as the quotient of the type `List α` by the equivalence relation of list permutation, effectively forgetting the order of elements while retaining their multiplicities.

Multiset.ofList definition

: List α → Multiset α

Full source

/-- The quotient map from `List α` to `Multiset α`. -/
@[coe]
def ofList : List α → Multiset α :=
  Quot.mk _

Multiset construction from a list

Informal description

The function that maps a list `[a₁, a₂, ..., aₙ]` to the multiset `{a₁, a₂, ..., aₙ}`, where the order of elements is forgotten but multiplicities are preserved.

Multiset.instCoeList instance

: Coe (List α) (Multiset α)

Full source

instance : Coe (List α) (Multiset α) :=
  ⟨ofList⟩

Canonical Multiset Construction from Lists

Informal description

For any type $\alpha$, there is a canonical way to view a list of elements of $\alpha$ as a multiset over $\alpha$, where the order of elements is forgotten but multiplicities are preserved.

Multiset.quot_mk_to_coe theorem

(l : List α) : @Eq (Multiset α) ⟦l⟧ l

Full source

@[simp]
theorem quot_mk_to_coe (l : List α) : @Eq (Multiset α) ⟦l⟧ l :=
  rfl

Equivalence of Quotient Construction and Multiset from List

Informal description

For any list $l$ of elements of type $\alpha$, the equivalence class of $l$ under the permutation relation is equal to the multiset constructed from $l$, i.e., $\llbracket l \rrbracket = l$ as multisets.

Multiset.quot_mk_to_coe' theorem

(l : List α) : @Eq (Multiset α) (Quot.mk (· ≈ ·) l) l

Full source

@[simp]
theorem quot_mk_to_coe' (l : List α) : @Eq (Multiset α) (Quot.mk (· ≈ ·) l) l :=
  rfl

Equivalence of Quotient Construction and Multiset from List

Informal description

For any list `l` of elements of type `α`, the equivalence class of `l` under the permutation relation is equal to the multiset constructed from `l`, i.e., $\text{Quot.mk} (\approx) l = l$ as multisets.

Multiset.quot_mk_to_coe'' theorem

(l : List α) : @Eq (Multiset α) (Quot.mk Setoid.r l) l

Full source

@[simp]
theorem quot_mk_to_coe'' (l : List α) : @Eq (Multiset α) (Quot.mk Setoid.r l) l :=
  rfl

Multiset Construction from List via Quotient Equals Direct Construction

Informal description

For any list $l$ of elements of type $\alpha$, the equivalence class of $l$ under the permutation relation is equal to the multiset constructed from $l$, i.e., $\text{Quot.mk Setoid.r } l = l$ as multisets.

Multiset.lift_coe theorem

 {α β : Type*} (x : List α) (f : List α → β) (h : ∀ a b : List α, a ≈ b → f a = f b) :
  Quotient.lift f h (x : Multiset α) = f x

Full source

@[simp]
theorem lift_coe {α β : Type*} (x : List α) (f : List α → β)
    (h : ∀ a b : List α, a ≈ b → f a = f b) : Quotient.lift f h (x : Multiset α) = f x :=
  Quotient.lift_mk _ _ _

Lift of Permutation-Respecting Function Preserves Evaluation on Multiset from List

Informal description

Let $\alpha$ and $\beta$ be types, $x$ be a list of elements of type $\alpha$, and $f : \text{List } \alpha \to \beta$ be a function that respects list permutation (i.e., $f(a) = f(b)$ whenever $a \sim b$). Then the lift of $f$ to multisets, when evaluated at the multiset corresponding to $x$, equals $f(x)$. In symbols: \[ \text{Quotient.lift}\, f\, h\, [x] = f(x) \] where $[x]$ denotes the multiset obtained from $x$ by forgetting the order of elements.

Multiset.coe_eq_coe theorem

{l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ ~ l₂

Full source

@[simp]
theorem coe_eq_coe {l₁ l₂ : List α} : (l₁ : Multiset α) = l₂ ↔ l₁ ~ l₂ :=
  Quotient.eq

Multiset Equality via List Permutation

Informal description

For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the corresponding multisets are equal if and only if $l_1$ is a permutation of $l_2$. In symbols: $$[l_1] = [l_2] \leftrightarrow l_1 \sim l_2$$ where $[l]$ denotes the multiset obtained from list $l$ by forgetting the order of elements.

Multiset.instDecidableEquivListOfDecidableEq instance

[DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂)

Full source

instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ ≈ l₂) :=
  inferInstanceAs (Decidable (l₁ ~ l₂))

Decidability of Multiset Equivalence for Lists

Informal description

For any type $\alpha$ with decidable equality, given two lists $l_1$ and $l_2$ in $\alpha$, it is decidable whether $l_1$ and $l_2$ are equivalent as multisets (i.e., whether one is a permutation of the other).

Multiset.instDecidableRListOfDecidableEq instance

[DecidableEq α] (l₁ l₂ : List α) : Decidable (isSetoid α l₁ l₂)

Full source

instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (isSetoid α l₁ l₂) :=
  inferInstanceAs (Decidable (l₁ ~ l₂))

Decidability of List Permutation for Multisets

Informal description

For any type α with decidable equality, given two lists l₁ and l₂ of elements in α, it is decidable whether l₁ and l₂ are equivalent under the multiset relation (i.e., whether they are permutations of each other).

Multiset.decidableEq instance

[DecidableEq α] : DecidableEq (Multiset α)

Full source

instance decidableEq [DecidableEq α] : DecidableEq (Multiset α)
  | s₁, s₂ => Quotient.recOnSubsingleton₂ s₁ s₂ fun _ _ => decidable_of_iff' _ Quotient.eq_iff_equiv

Decidability of Multiset Equality

Informal description

For any type $\alpha$ with decidable equality, the equality of multisets over $\alpha$ is decidable.

Multiset.Mem definition

(s : Multiset α) (a : α) : Prop

Full source

/-- `a ∈ s` means that `a` has nonzero multiplicity in `s`. -/
def Mem (s : Multiset α) (a : α) : Prop :=
  Quot.liftOn s (fun l => a ∈ l) fun l₁ l₂ (e : l₁ ~ l₂) => propext <| e.mem_iff

Membership in a multiset

Informal description

Given a multiset $ s $ over a type $ \alpha $ and an element $ a \in \alpha $, the proposition $ a \in s $ (read as "$ a $ is a member of $ s $") holds if and only if $ a $ appears with nonzero multiplicity in $ s $. This is defined by lifting the list membership relation to multisets via the quotient construction, ensuring that the membership relation is well-defined under permutations of the underlying list representation.

Multiset.instMembership instance

: Membership α (Multiset α)

Full source

instance : Membership α (Multiset α) :=
  ⟨Mem⟩

Membership Relation for Multisets

Informal description

For any type $\alpha$, there is a membership relation $\in$ between elements of $\alpha$ and multisets over $\alpha$, where $a \in s$ holds if and only if the element $a$ appears with nonzero multiplicity in the multiset $s$.

Multiset.mem_coe theorem

{a : α} {l : List α} : a ∈ (l : Multiset α) ↔ a ∈ l

Full source

@[simp]
theorem mem_coe {a : α} {l : List α} : a ∈ (l : Multiset α)a ∈ (l : Multiset α) ↔ a ∈ l :=
  Iff.rfl

Membership in Multiset from List Coercion

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of $\alpha$, the element $a$ belongs to the multiset constructed from $l$ (denoted by the coercion $(l : \text{Multiset } \alpha)$) if and only if $a$ is a member of the list $l$.

Multiset.decidableMem instance

[DecidableEq α] (a : α) (s : Multiset α) : Decidable (a ∈ s)

Full source

instance decidableMem [DecidableEq α] (a : α) (s : Multiset α) : Decidable (a ∈ s) :=
  Quot.recOnSubsingleton s fun l ↦ inferInstanceAs (Decidable (a ∈ l))

Decidability of Membership in Multisets

Informal description

For any type $\alpha$ with decidable equality and any element $a \in \alpha$, the membership relation $a \in s$ in a multiset $s$ is decidable.

Multiset.Subset definition

(s t : Multiset α) : Prop

Full source

/-- `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. -/
protected def Subset (s t : Multiset α) : Prop :=
  ∀ ⦃a : α⦄, a ∈ s → a ∈ t

Subset relation for multisets

Informal description

For two multisets $s$ and $t$ over a type $\alpha$, the subset relation $s \subseteq t$ holds if every element $a$ that appears in $s$ (i.e., has nonzero multiplicity) also appears in $t$ (i.e., has nonzero multiplicity). Note that this does not require the multiplicity of $a$ in $s$ to be less than or equal to its multiplicity in $t$; for that stronger relation, see the partial order $\leq$ on multisets.

Multiset.instHasSubset instance

: HasSubset (Multiset α)

Full source

instance : HasSubset (Multiset α) :=
  ⟨Multiset.Subset⟩

Subset Relation on Multisets

Informal description

The type of multisets over any type $\alpha$ is equipped with a subset relation $\subseteq$, where for two multisets $s$ and $t$, $s \subseteq t$ holds if every element in $s$ also appears in $t$ (with nonzero multiplicity).

Multiset.instHasSSubset instance

: HasSSubset (Multiset α)

Full source

instance : HasSSubset (Multiset α) :=
  ⟨fun s t => s ⊆ t ∧ ¬t ⊆ s⟩

Strict Subset Relation on Multisets

Informal description

The type of multisets over any type $\alpha$ is equipped with a strict subset relation $\subset$, where for two multisets $s$ and $t$, $s \subset t$ holds if $s$ is a subset of $t$ but $s \neq t$.

Multiset.instIsNonstrictStrictOrder instance

: IsNonstrictStrictOrder (Multiset α) (· ⊆ ·) (· ⊂ ·)

Full source

instance instIsNonstrictStrictOrder : IsNonstrictStrictOrder (Multiset α) (· ⊆ ·) (· ⊂ ·) where
  right_iff_left_not_left _ _ := Iff.rfl

Subset and Strict Subset Form Nonstrict-Strict Order on Multisets

Informal description

For any type $\alpha$, the subset relation $\subseteq$ and the strict subset relation $\subset$ on multisets over $\alpha$ form a nonstrict-strict order pair. This means that for any two multisets $s$ and $t$, $s \subset t$ if and only if $s \subseteq t$ and $s \neq t$.

Multiset.coe_subset theorem

{l₁ l₂ : List α} : (l₁ : Multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂

Full source

@[simp]
theorem coe_subset {l₁ l₂ : List α} : (l₁ : Multiset α) ⊆ l₂(l₁ : Multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂ :=
  Iff.rfl

Subset Correspondence Between Lists and Multisets: $l₁ \subseteq l₂$ iff $\{l₁\} \subseteq \{l₂\}$

Informal description

For any two lists $l₁$ and $l₂$ of elements of type $\alpha$, the multiset obtained from $l₁$ is a subset of the multiset obtained from $l₂$ if and only if $l₁$ is a subset of $l₂$ as lists (i.e., every element of $l₁$ appears in $l₂$).

Multiset.Subset.refl theorem

(s : Multiset α) : s ⊆ s

Full source

@[simp]
theorem Subset.refl (s : Multiset α) : s ⊆ s := fun _ h => h

Reflexivity of Multiset Subset Relation

Informal description

For any multiset $s$ over a type $\alpha$, the subset relation is reflexive, i.e., $s \subseteq s$.

Multiset.Subset.trans theorem

{s t u : Multiset α} : s ⊆ t → t ⊆ u → s ⊆ u

Full source

theorem Subset.trans {s t u : Multiset α} : s ⊆ t → t ⊆ u → s ⊆ u := fun h₁ h₂ _ m => h₂ (h₁ m)

Transitivity of Multiset Subset Relation

Informal description

For any multisets $s, t, u$ over a type $\alpha$, if $s \subseteq t$ and $t \subseteq u$, then $s \subseteq u$.

Multiset.subset_iff theorem

{s t : Multiset α} : s ⊆ t ↔ ∀ ⦃x⦄, x ∈ s → x ∈ t

Full source

theorem subset_iff {s t : Multiset α} : s ⊆ ts ⊆ t ↔ ∀ ⦃x⦄, x ∈ s → x ∈ t :=
  Iff.rfl

Characterization of Multiset Subset Relation

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the subset relation $s \subseteq t$ holds if and only if every element $x$ that belongs to $s$ (with nonzero multiplicity) also belongs to $t$.

Multiset.mem_of_subset theorem

{s t : Multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a ∈ t

Full source

theorem mem_of_subset {s t : Multiset α} {a : α} (h : s ⊆ t) : a ∈ s → a ∈ t :=
  @h _

Subset Membership Preservation in Multisets

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, and any element $a \in \alpha$, if $s$ is a subset of $t$ and $a$ is an element of $s$, then $a$ is also an element of $t$.

Multiset.Le definition

(s t : Multiset α) : Prop

Full source

/-- `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`. -/
protected def Le (s t : Multiset α) : Prop :=
  (Quotient.liftOn₂ s t (· <+~ ·)) fun _ _ _ _ p₁ p₂ =>
    propext (p₂.subperm_left.trans p₁.subperm_right)

Sub-multiset relation

Informal description

For two multisets $s$ and $t$ over a type $\alpha$, the relation $s \leq t$ holds if and only if the count of every element $a$ in $s$ is less than or equal to its count in $t$. This defines a partial order on multisets, where $s$ is considered a sub-multiset of $t$.

Multiset.instPartialOrder instance

: PartialOrder (Multiset α)

Full source

instance : PartialOrder (Multiset α) where
  le := Multiset.Le
  le_refl := by rintro ⟨l⟩; exact Subperm.refl _
  le_trans := by rintro ⟨l₁⟩ ⟨l₂⟩ ⟨l₃⟩; exact @Subperm.trans _ _ _ _
  le_antisymm := by rintro ⟨l₁⟩ ⟨l₂⟩ h₁ h₂; exact Quot.sound (Subperm.antisymm h₁ h₂)

Partial Order on Multisets

Informal description

The type of multisets over any type $\alpha$ forms a partial order under the sub-multiset relation $\leq$, where $s \leq t$ if and only if every element in $s$ has a multiplicity in $s$ less than or equal to its multiplicity in $t$.

Multiset.decidableLE instance

[DecidableEq α] : DecidableLE (Multiset α)

Full source

instance decidableLE [DecidableEq α] : DecidableLE (Multiset α) :=
  fun s t => Quotient.recOnSubsingleton₂ s t List.decidableSubperm

Decidability of Sub-multiset Relation

Informal description

For any type $\alpha$ with decidable equality, the sub-multiset relation $\leq$ on multisets over $\alpha$ is decidable.

Multiset.subset_of_le theorem

: s ≤ t → s ⊆ t

Full source

theorem subset_of_le : s ≤ t → s ⊆ t :=
  Quotient.inductionOn₂ s t fun _ _ => Subperm.subset

Sub-multiset Implies Subset for Multisets

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ is a sub-multiset of $t$ (i.e., $s \leq t$), then $s$ is a subset of $t$ (i.e., $s \subseteq t$). In other words, if every element in $s$ has multiplicity in $s$ less than or equal to its multiplicity in $t$, then every element with nonzero multiplicity in $s$ also has nonzero multiplicity in $t$.

Multiset.mem_of_le theorem

(h : s ≤ t) : a ∈ s → a ∈ t

Full source

theorem mem_of_le (h : s ≤ t) : a ∈ s → a ∈ t :=
  mem_of_subset (subset_of_le h)

Sub-multiset Preserves Membership

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, and any element $a \in \alpha$, if $s$ is a sub-multiset of $t$ (i.e., $s \leq t$) and $a$ is an element of $s$, then $a$ is also an element of $t$.

Multiset.not_mem_mono theorem

(h : s ⊆ t) : a ∉ t → a ∉ s

Full source

theorem not_mem_mono (h : s ⊆ t) : a ∉ t → a ∉ s :=
  mt <| @h _

Contrapositive of Subset Membership for Multisets

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$ (i.e., $s \subseteq t$), then for any element $a \in \alpha$, if $a$ is not in $t$ (i.e., $a \notin t$), then $a$ is not in $s$ (i.e., $a \notin s$).

Multiset.coe_le theorem

{l₁ l₂ : List α} : (l₁ : Multiset α) ≤ l₂ ↔ l₁ <+~ l₂

Full source

@[simp]
theorem coe_le {l₁ l₂ : List α} : (l₁ : Multiset α) ≤ l₂ ↔ l₁ <+~ l₂ :=
  Iff.rfl

Multiset Order via Subpermutation of Lists

Informal description

For any two lists `l₁` and `l₂` of elements of type `α`, the multiset obtained from `l₁` is less than or equal to the multiset obtained from `l₂` if and only if `l₁` is a subpermutation of `l₂`. Here, a subpermutation `l₁ <+~ l₂` means that `l₁` can be obtained from `l₂` by deleting some elements (possibly none) and permuting the remaining ones.

Multiset.leInductionOn theorem

 {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t) (H : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → C l₁ l₂) :
  C s t

Full source

@[elab_as_elim]
theorem leInductionOn {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t)
    (H : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → C l₁ l₂) : C s t :=
  Quotient.inductionOn₂ s t (fun l₁ _ ⟨l, p, s⟩ => (show ⟦l⟧ = ⟦l₁⟧ from Quot.sound p) ▸ H s) h

Induction Principle for Sub-Multiset Order via Sublists

Informal description

Let $C$ be a predicate on pairs of multisets over a type $\alpha$, and let $s$ and $t$ be multisets such that $s \leq t$ in the sub-multiset order. If for any two lists $l₁$ and $l₂$ of elements of $\alpha$, the condition $l₁$ is a sublist of $l₂$ implies $C(l₁, l₂)$, then $C(s, t)$ holds.

Multiset.card definition

: Multiset α → ℕ

Full source

/-- The cardinality of a multiset is the sum of the multiplicities
  of all its elements, or simply the length of the underlying list. -/
def card : Multiset α → ℕ := Quot.lift length fun _l₁ _l₂ => Perm.length_eq

Cardinality of a multiset

Informal description

The function `Multiset.card` maps a multiset to its cardinality, which is the sum of the multiplicities of all its elements (or equivalently, the length of any underlying list representing the multiset up to permutation).

Multiset.coe_card theorem

(l : List α) : card (l : Multiset α) = length l

Full source

@[simp]
theorem coe_card (l : List α) : card (l : Multiset α) = length l :=
  rfl

Multiset Cardinality Equals List Length

Informal description

For any list $l$ of elements of type $\alpha$, the cardinality of the multiset obtained from $l$ is equal to the length of $l$, i.e., $\text{card}(\{l\}) = \text{length}(l)$.

Multiset.card_le_card theorem

{s t : Multiset α} (h : s ≤ t) : card s ≤ card t

Full source

theorem card_le_card {s t : Multiset α} (h : s ≤ t) : card s ≤ card t :=
  leInductionOn h Sublist.length_le

Sub-multiset Implies Cardinality Inequality: $s \leq t \implies \text{card}(s) \leq \text{card}(t)$

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ is a sub-multiset of $t$ (i.e., $s \leq t$), then the cardinality of $s$ is less than or equal to the cardinality of $t$.

Multiset.card_lt_card theorem

{s t : Multiset α} (h : s < t) : card s < card t

Full source

theorem card_lt_card {s t : Multiset α} (h : s < t) : card s < card t :=
  lt_of_not_ge fun h₂ => _root_.ne_of_lt h <| eq_of_le_of_card_le (le_of_lt h) h₂

Strict Sub-multiset Implies Strict Cardinality Inequality: $s < t \implies \text{card}(s) < \text{card}(t)$

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, if $s$ is a strict sub-multiset of $t$ (i.e., $s < t$), then the cardinality of $s$ is strictly less than the cardinality of $t$.

Multiset.card_mono theorem

: Monotone (@card α)

Full source

@[mono]
theorem card_mono : Monotone (@card α) := fun _a _b => card_le_card

Monotonicity of Multiset Cardinality: $s \leq t \implies \text{card}(s) \leq \text{card}(t)$

Informal description

The cardinality function on multisets is monotone with respect to the sub-multiset relation. That is, for any two multisets $s$ and $t$ over a type $\alpha$, if $s \leq t$ (meaning every element in $s$ has multiplicity at least as large in $t$), then the cardinality of $s$ is less than or equal to the cardinality of $t$, i.e., $\text{card}(s) \leq \text{card}(t)$.

Multiset.card_strictMono theorem

: StrictMono (card : Multiset α → ℕ)

Full source

lemma card_strictMono : StrictMono (card : Multiset α → ℕ) := fun _ _ ↦ card_lt_card

Strict Monotonicity of Multiset Cardinality: $s < t \implies \text{card}(s) < \text{card}(t)$

Informal description

The cardinality function $\text{card} : \text{Multiset } \alpha \to \mathbb{N}$ is strictly monotone with respect to the sub-multiset relation. That is, for any two multisets $s$ and $t$ over a type $\alpha$, if $s < t$, then $\text{card}(s) < \text{card}(t)$.

Multiset.instWellFoundedLT instance

: WellFoundedLT (Multiset α)

Full source

/-- Another way of expressing `strongInductionOn`: the `(<)` relation is well-founded. -/
instance instWellFoundedLT : WellFoundedLT (Multiset α) :=
  ⟨Subrelation.wf Multiset.card_lt_card (measure Multiset.card).2⟩

Well-foundedness of the Strict Sub-multiset Relation

Informal description

The strict sub-multiset relation `<` on multisets is well-founded. That is, every non-empty collection of multisets over a type $\alpha$ has a minimal element with respect to the strict sub-multiset relation.

Multiset.coe_reverse theorem

(l : List α) : (reverse l : Multiset α) = l

Full source

@[simp]
theorem coe_reverse (l : List α) : (reverse l : Multiset α) = l :=
  Quot.sound <| reverse_perm _

Multiset Construction Preserves Equality Under List Reversal

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained by reversing $l$ is equal to the multiset obtained from $l$ itself. In other words, the multiset construction forgets the order of elements in the list.

Multiset.pmap definition

{p : α → Prop} (f : ∀ a, p a → β) (s : Multiset α) : (∀ a ∈ s, p a) → Multiset β

Full source

/-- Lift of the list `pmap` operation. Map a partial function `f` over a multiset
  `s` whose elements are all in the domain of `f`. -/
nonrec def pmap {p : α → Prop} (f : ∀ a, p a → β) (s : Multiset α) : (∀ a ∈ s, p a) → Multiset β :=
  Quot.recOn s (fun l H => ↑(pmap f l H)) fun l₁ l₂ (pp : l₁ ~ l₂) =>
    funext fun H₂ : ∀ a ∈ l₂, p a =>
      have H₁ : ∀ a ∈ l₁, p a := fun a h => H₂ a (pp.subset h)
      have : ∀ {s₂ e H}, @Eq.ndrec (Multiset α) l₁ (fun s => (∀ a ∈ s, p a) → Multiset β)
          (fun _ => ↑(pmap f l₁ H₁)) s₂ e H = ↑(pmap f l₁ H₁) := by
        intro s₂ e _; subst e; rfl
      this.trans <| Quot.sound <| pp.pmap f

Partial function map for multisets

Informal description

Given a predicate `p : α → Prop` and a function `f` defined on all elements of `α` satisfying `p`, the function `Multiset.pmap` maps a multiset `s` over `α` to a multiset over `β`, provided that every element in `s` satisfies `p`. Specifically, for each element `a ∈ s`, `f` is applied to `a` and its proof of `p a` to produce an element of `β`, and these results are collected into a new multiset.

Multiset.coe_pmap theorem

{p : α → Prop} (f : ∀ a, p a → β) (l : List α) (H : ∀ a ∈ l, p a) : pmap f l H = l.pmap f H

Full source

@[simp]
theorem coe_pmap {p : α → Prop} (f : ∀ a, p a → β) (l : List α) (H : ∀ a ∈ l, p a) :
    pmap f l H = l.pmap f H :=
  rfl

Equality of Multiset Partial Map and List Partial Map

Informal description

Given a predicate $p : \alpha \to \text{Prop}$ and a function $f : (\forall a, p a \to \beta)$, for any list $l$ of elements of type $\alpha$ where every element $a \in l$ satisfies $p a$, the multiset obtained by applying the partial map $f$ to $l$ is equal to the multiset obtained by applying the list's partial map operation to $l$ with $f$.

Multiset.pmap_congr theorem

 {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (s : Multiset α) :
  ∀ {H₁ H₂}, (∀ a ∈ s, ∀ (h₁ h₂), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂

Full source

theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (s : Multiset α) :
    ∀ {H₁ H₂}, (∀ a ∈ s, ∀ (h₁ h₂), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂ :=
  @(Quot.inductionOn s (fun l _H₁ _H₂ h => congr_arg _ <| List.pmap_congr_left l h))

Congruence of Partial Multiset Maps under Pointwise Equality

Informal description

For any type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, functions $f : (\forall a, p a \to \beta)$ and $g : (\forall a, q a \to \beta)$, and multiset $s$ over $\alpha$, if for every element $a \in s$ and any proofs $h_1 : p a$ and $h_2 : q a$ we have $f a h_1 = g a h_2$, then the partial maps $\text{pmap}\, f\, s\, H_1$ and $\text{pmap}\, g\, s\, H_2$ are equal.

Multiset.mem_pmap theorem

{p : α → Prop} {f : ∀ a, p a → β} {s H b} : b ∈ pmap f s H ↔ ∃ (a : _) (h : a ∈ s), f a (H a h) = b

Full source

@[simp]
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {s H b} :
    b ∈ pmap f s Hb ∈ pmap f s H ↔ ∃ (a : _) (h : a ∈ s), f a (H a h) = b :=
  Quot.inductionOn s (fun _l _H => List.mem_pmap) H

Membership in Partial Multiset Map via Preimage

Informal description

For a predicate $p : \alpha \to \text{Prop}$, a function $f : (\forall a, p a \to \beta)$, a multiset $s$ over $\alpha$, and a proof $H$ that all elements of $s$ satisfy $p$, an element $b$ belongs to the multiset $\text{pmap}\, f\, s\, H$ if and only if there exists an element $a \in s$ such that $f$ applied to $a$ and its proof $H a h$ yields $b$. In other words: $$b \in \text{pmap}\, f\, s\, H \leftrightarrow \exists (a \in s), f a (H a h) = b.$$

Multiset.card_pmap theorem

{p : α → Prop} (f : ∀ a, p a → β) (s H) : card (pmap f s H) = card s

Full source

@[simp]
theorem card_pmap {p : α → Prop} (f : ∀ a, p a → β) (s H) : card (pmap f s H) = card s :=
  Quot.inductionOn s (fun _l _H => length_pmap) H

Cardinality Preservation under Partial Multiset Mapping

Informal description

For any predicate $p : \alpha \to \text{Prop}$, function $f : (\forall a, p a \to \beta)$, multiset $s$ over $\alpha$, and proof $H$ that all elements of $s$ satisfy $p$, the cardinality of the multiset obtained by applying $f$ to each element of $s$ (with its proof) is equal to the cardinality of $s$. That is, $|\text{pmap}\, f\, s\, H| = |s|$.

Multiset.attach definition

(s : Multiset α) : Multiset { x // x ∈ s }

Full source

/-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce
  a multiset on `{x // x ∈ s}`. -/
def attach (s : Multiset α) : Multiset { x // x ∈ s } :=
  pmap Subtype.mk s fun _a => id

Multiset with attached membership proofs

Informal description

Given a multiset $s$ over a type $\alpha$, the function `Multiset.attach` produces a multiset over the subtype $\{x \mid x \in s\}$ by attaching to each element $a \in s$ a proof that $a$ is indeed an element of $s$. This effectively creates a multiset where each element is paired with its membership proof in $s$.

Multiset.coe_attach theorem

(l : List α) : @Eq (Multiset { x // x ∈ l }) (@attach α l) l.attach

Full source

@[simp]
theorem coe_attach (l : List α) : @Eq (Multiset { x // x ∈ l }) (@attach α l) l.attach :=
  rfl

Equality of Attached Multisets from List Conversion

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained by attaching membership proofs to each element of $l$ is equal to the multiset obtained by first converting $l$ to a multiset and then attaching membership proofs. In other words, $\text{attach}(\text{ofList}(l)) = \text{ofList}(l.\text{attach})$.

Multiset.mem_attach theorem

(s : Multiset α) : ∀ x, x ∈ s.attach

Full source

@[simp]
theorem mem_attach (s : Multiset α) : ∀ x, x ∈ s.attach :=
  Quot.inductionOn s fun _l => List.mem_attach _

Membership in Attached Multiset

Informal description

For any multiset $s$ over a type $\alpha$, every element $x$ in the attached multiset $s.\text{attach}$ satisfies $x \in s.\text{attach}$.

Multiset.card_attach theorem

{m : Multiset α} : card (attach m) = card m

Full source

@[simp]
theorem card_attach {m : Multiset α} : card (attach m) = card m :=
  card_pmap _ _ _

Cardinality Preservation under Multiset Attachment

Informal description

For any multiset $m$ over a type $\alpha$, the cardinality of the multiset obtained by attaching membership proofs (i.e., $\text{attach}\, m$) is equal to the cardinality of $m$ itself. In other words, $|\text{attach}\, m| = |m|$.

Multiset.decidableForallMultiset definition

{p : α → Prop} [∀ a, Decidable (p a)] : Decidable (∀ a ∈ m, p a)

Full source

/-- If `p` is a decidable predicate,
so is the predicate that all elements of a multiset satisfy `p`. -/
protected def decidableForallMultiset {p : α → Prop} [∀ a, Decidable (p a)] :
    Decidable (∀ a ∈ m, p a) :=
  Quotient.recOnSubsingleton m fun l => decidable_of_iff (∀ a ∈ l, p a) <| by simp

Decidability of universal quantification over a multiset

Informal description

Given a decidable predicate $p$ on elements of type $\alpha$, the predicate "for all elements $a$ in the multiset $m$, $p(a)$ holds" is also decidable. This means we can algorithmically determine whether all elements of $m$ satisfy $p$.

Multiset.decidableDforallMultiset instance

{p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a ∈ m), Decidable (p a h)] : Decidable (∀ (a) (h : a ∈ m), p a h)

Full source

instance decidableDforallMultiset {p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a ∈ m), Decidable (p a h)] :
    Decidable (∀ (a) (h : a ∈ m), p a h) :=
  @decidable_of_iff _ _
    (Iff.intro (fun h a ha => h ⟨a, ha⟩ (mem_attach _ _)) fun h ⟨_a, _ha⟩ _ => h _ _)
    (@Multiset.decidableForallMultiset _ m.attach (fun a => p a.1 a.2) _)

Decidability of Dependent Universal Quantification over a Multiset

Informal description

For any multiset $m$ over a type $\alpha$ and a dependent predicate $p$ on elements of $m$ (where for each $a \in m$, $p(a)$ is a proposition depending on the proof that $a \in m$), if $p(a)$ is decidable for every $a \in m$, then the universal statement "for all $a \in m$, $p(a)$ holds" is also decidable.

Multiset.decidableEqPiMultiset instance

{β : α → Type*} [∀ a, DecidableEq (β a)] : DecidableEq (∀ a ∈ m, β a)

Full source

/-- decidable equality for functions whose domain is bounded by multisets -/
instance decidableEqPiMultiset {β : α → Type*} [∀ a, DecidableEq (β a)] :
    DecidableEq (∀ a ∈ m, β a) := fun f g =>
  decidable_of_iff (∀ (a) (h : a ∈ m), f a h = g a h) (by simp [funext_iff])

Decidable Equality for Functions on Multisets

Informal description

For any multiset $m$ over a type $\alpha$ and any family of types $\beta : \alpha \to \text{Type}^*$ where each $\beta a$ has decidable equality, the equality of functions $f, g : \forall a \in m, \beta a$ is decidable.

Multiset.decidableExistsMultiset definition

{p : α → Prop} [DecidablePred p] : Decidable (∃ x ∈ m, p x)

Full source

/-- If `p` is a decidable predicate,
so is the existence of an element in a multiset satisfying `p`. -/
protected def decidableExistsMultiset {p : α → Prop} [DecidablePred p] : Decidable (∃ x ∈ m, p x) :=
  Quotient.recOnSubsingleton m fun l => decidable_of_iff (∃ a ∈ l, p a) <| by simp

Decidability of existence in a multiset

Informal description

Given a decidable predicate $p$ on elements of type $\alpha$, the decidability of the existence of an element $x$ in a multiset $m$ such that $p(x)$ holds is established. This means we can algorithmically determine whether there exists at least one element in $m$ satisfying $p$.

Multiset.decidableDexistsMultiset instance

{p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a ∈ m), Decidable (p a h)] : Decidable (∃ (a : _) (h : a ∈ m), p a h)

Full source

instance decidableDexistsMultiset {p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a ∈ m), Decidable (p a h)] :
    Decidable (∃ (a : _) (h : a ∈ m), p a h) :=
  @decidable_of_iff _ _
    (Iff.intro (fun ⟨⟨a, ha₁⟩, _, ha₂⟩ => ⟨a, ha₁, ha₂⟩) fun ⟨a, ha₁, ha₂⟩ =>
      ⟨⟨a, ha₁⟩, mem_attach _ _, ha₂⟩)
    (@Multiset.decidableExistsMultiset { a // a ∈ m } m.attach (fun a => p a.1 a.2) _)

Decidability of Dependent Existence in Multisets

Informal description

For any multiset $m$ over a type $\alpha$ and a decidable predicate $p$ on elements of $m$, it is decidable whether there exists an element $a \in m$ and a proof $h$ that $a \in m$ such that $p(a, h)$ holds.

Multiset.Pairwise definition

(r : α → α → Prop) (m : Multiset α) : Prop

Full source

/-- `Pairwise r m` states that there exists a list of the elements s.t. `r` holds pairwise on this
list. -/
def Pairwise (r : α → α → Prop) (m : Multiset α) : Prop :=
  ∃ l : List α, m = l ∧ l.Pairwise r

Pairwise relation on a multiset

Informal description

A multiset $m$ satisfies `Pairwise r` if there exists a list $l$ whose elements form the multiset $m$ (i.e., $m$ is the quotient of $l$ under permutation) and the relation $r$ holds pairwise for all distinct elements in $l$. In other words, $r$ must hold between any two distinct elements of some representative list of $m$.

Multiset.pairwise_coe_iff theorem

{r : α → α → Prop} {l : List α} : Multiset.Pairwise r l ↔ ∃ l' : List α, l ~ l' ∧ l'.Pairwise r

Full source

theorem pairwise_coe_iff {r : α → α → Prop} {l : List α} :
    Multiset.PairwiseMultiset.Pairwise r l ↔ ∃ l' : List α, l ~ l' ∧ l'.Pairwise r :=
  exists_congr <| by simp

Equivalence of Multiset Pairwise and List Pairwise via Permutation

Informal description

For any relation $r$ on elements of type $\alpha$ and any list $l$ of type $\alpha$, the multiset formed from $l$ satisfies the pairwise relation $\text{Multiset.Pairwise}\, r$ if and only if there exists a list $l'$ that is a permutation of $l$ and satisfies the pairwise relation $r$ on its elements.

Multiset.pairwise_coe_iff_pairwise theorem

{r : α → α → Prop} (hr : Symmetric r) {l : List α} : Multiset.Pairwise r l ↔ l.Pairwise r

Full source

theorem pairwise_coe_iff_pairwise {r : α → α → Prop} (hr : Symmetric r) {l : List α} :
    Multiset.PairwiseMultiset.Pairwise r l ↔ l.Pairwise r :=
  Iff.intro (fun ⟨_l', Eq, h⟩ => ((Quotient.exact Eq).pairwise_iff @hr).2 h) fun h => ⟨l, rfl, h⟩

Equivalence of Multiset and List Pairwise Relations for Symmetric Relations

Informal description

For any symmetric relation $r$ on a type $\alpha$ and any list $l$ of elements of type $\alpha$, the multiset formed from $l$ satisfies the pairwise relation $r$ if and only if the list $l$ itself satisfies the pairwise relation $r$.

Multiset.Nodup definition

(s : Multiset α) : Prop

Full source

/-- `Nodup s` means that `s` has no duplicates, i.e. the multiplicity of
  any element is at most 1. -/
def Nodup (s : Multiset α) : Prop :=
  Quot.liftOn s List.Nodup fun _ _ p => propext p.nodup_iff

Multiset without duplicates

Informal description

A multiset `s` is called *nodup* (no duplicates) if every element in `s` has multiplicity at most 1, meaning no element appears more than once in `s`. This is equivalent to saying that `s` can be represented by a list without duplicate elements.

Multiset.coe_nodup theorem

{l : List α} : @Nodup α l ↔ l.Nodup

Full source

@[simp]
theorem coe_nodup {l : List α} : @Nodup α l ↔ l.Nodup :=
  Iff.rfl

Equivalence of Duplicate-Free Property Between Lists and Multisets

Informal description

For any list `l` of elements of type `α`, the multiset constructed from `l` has no duplicates if and only if the list `l` itself has no duplicate elements. In other words, the property of being duplicate-free is preserved when converting a list to a multiset.

Multiset.Nodup.ext theorem

{s t : Multiset α} : Nodup s → Nodup t → (s = t ↔ ∀ a, a ∈ s ↔ a ∈ t)

Full source

theorem Nodup.ext {s t : Multiset α} : Nodup s → Nodup t → (s = t ↔ ∀ a, a ∈ s ↔ a ∈ t) :=
  Quotient.inductionOn₂ s t fun _ _ d₁ d₂ => Quotient.eq.trans <| perm_ext_iff_of_nodup d₁ d₂

Equality of Duplicate-Free Multisets via Membership

Informal description

For any two duplicate-free multisets $s$ and $t$ over a type $\alpha$, the following are equivalent: 1. $s = t$ (the multisets are equal) 2. For every element $a \in \alpha$, $a$ belongs to $s$ if and only if $a$ belongs to $t$.

Multiset.le_iff_subset theorem

{s t : Multiset α} : Nodup s → (s ≤ t ↔ s ⊆ t)

Full source

theorem le_iff_subset {s t : Multiset α} : Nodup s → (s ≤ t ↔ s ⊆ t) :=
  Quotient.inductionOn₂ s t fun _ _ d => ⟨subset_of_le, d.subperm⟩

Equivalence of Sub-multiset and Subset Relations for Duplicate-Free Multisets

Informal description

For any duplicate-free multisets $s$ and $t$ over a type $\alpha$, the sub-multiset relation $s \leq t$ holds if and only if $s$ is a subset of $t$ (i.e., every element in $s$ also appears in $t$ with nonzero multiplicity).

Multiset.nodup_of_le theorem

{s t : Multiset α} (h : s ≤ t) : Nodup t → Nodup s

Full source

theorem nodup_of_le {s t : Multiset α} (h : s ≤ t) : Nodup t → Nodup s :=
  Multiset.leInductionOn h fun {_ _} => Nodup.sublist

Sub-multiset preserves no-duplicates property

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, if $s$ is a sub-multiset of $t$ (i.e., $s \leq t$) and $t$ has no duplicate elements, then $s$ also has no duplicate elements.

Multiset.nodupDecidable instance

[DecidableEq α] (s : Multiset α) : Decidable (Nodup s)

Full source

instance nodupDecidable [DecidableEq α] (s : Multiset α) : Decidable (Nodup s) :=
  Quotient.recOnSubsingleton s fun l => l.nodupDecidable

Decidability of Duplicate-Free Multisets

Informal description

For any type $\alpha$ with decidable equality and any multiset $s$ over $\alpha$, the property of $s$ being duplicate-free (i.e., every element has multiplicity at most 1) is decidable.

Multiset.sizeOf definition

[SizeOf α] (s : Multiset α) : ℕ

Full source

/-- 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.
-/
protected
def sizeOf [SizeOf α] (s : Multiset α) : ℕ :=
  (Quot.liftOn s SizeOf.sizeOf) fun _ _ => Perm.sizeOf_eq_sizeOf

Size of a multiset

Informal description

The function `Multiset.sizeOf` computes the size of a multiset `s` by summing the sizes of its elements (counted with multiplicity). This is defined by lifting the size function from the underlying list representation of the multiset, ensuring that the size is invariant under permutations of the list.

Multiset.instSizeOf instance

[SizeOf α] : SizeOf (Multiset α)

Full source

instance [SizeOf α] : SizeOf (Multiset α) :=
  ⟨Multiset.sizeOf⟩

Size Function for Multisets

Informal description

For any type $\alpha$ with a size function, the multiset over $\alpha$ inherits a size function where the size of a multiset is the sum of the sizes of its elements (counting multiplicities).