doc-next-gen

Mathlib.Data.Multiset.Powerset

Module docstring

{"# The powerset of a multiset ","### powerset ","### powersetCard "}

Multiset.powersetAux definition
(l : List α) : List (Multiset α)
Full source 
/-- A helper function for the powerset of a multiset. Given a list `l`, returns a list
of sublists of `l` as multisets. -/
def powersetAux (l : List α) : List (Multiset α) :=
  (sublists l).map (↑)
List of sublist multisets
Informal description
Given a list `l` of elements of type `α`, the function returns a list of all sublists of `l` converted to multisets. More precisely, for any list `l`, the result is obtained by taking all sublists of `l` (via `sublists l`) and then converting each sublist to a multiset (via the canonical map `↑`).
Multiset.powersetAux_eq_map_coe theorem
{l : List α} : powersetAux l = (sublists l).map (↑)
Full source 
theorem powersetAux_eq_map_coe {l : List α} : powersetAux l = (sublists l).map (↑) :=
  rfl
Equivalence of `powersetAux` and Mapping Sublists to Multisets
Informal description
For any list `l` of elements of type `α`, the function `powersetAux l` is equal to the list obtained by mapping the canonical embedding from lists to multisets over all sublists of `l`. In other words, `powersetAux l = (sublists l).map (↑)`.
Multiset.mem_powersetAux theorem
{l : List α} {s} : s ∈ powersetAux l ↔ s ≤ ↑l
Full source 
@[simp]
theorem mem_powersetAux {l : List α} {s} : s ∈ powersetAux ls ∈ powersetAux l ↔ s ≤ ↑l :=
  Quotient.inductionOn s <| by simp [powersetAux_eq_map_coe, Subperm, and_comm]
Membership in Sublist Multisets is Equivalent to Submultiset Relation
Informal description
For any list $l$ of elements of type $\alpha$ and any multiset $s$, the multiset $s$ belongs to the list of sublist multisets `powersetAux l` if and only if $s$ is a submultiset of the multiset obtained from $l$ (denoted by $\uparrow l$).
Multiset.powersetAux' definition
(l : List α) : List (Multiset α)
Full source 
/-- Helper function for the powerset of a multiset. Given a list `l`, returns a list
of sublists of `l` (using `sublists'`), as multisets. -/
def powersetAux' (l : List α) : List (Multiset α) :=
  (sublists' l).map (↑)
Multiset of sublists of a list
Informal description
Given a list `l`, the function returns a list of all sublists of `l` (computed using `sublists'`), each represented as a multiset.
Multiset.powersetAux_perm_powersetAux' theorem
{l : List α} : powersetAux l ~ powersetAux' l
Full source 
theorem powersetAux_perm_powersetAux' {l : List α} : powersetAuxpowersetAux l ~ powersetAux' l := by
  rw [powersetAux_eq_map_coe]; exact (sublists_perm_sublists' _).map _
Permutation of Powerset Computations for Multisets
Informal description
For any list $l$ of elements of type $\alpha$, the list of sublist multisets obtained via `powersetAux l` is a permutation of the list obtained via `powersetAux' l$. In other words, the two computations of the powerset of $l$ (as multisets) yield lists that are rearrangements of each other, i.e., $\text{powersetAux}(l) \sim \text{powersetAux'}(l)$, where $\sim$ denotes the permutation relation between lists.
Multiset.powersetAux'_nil theorem
: powersetAux' (@nil α) = [0]
Full source 
@[simp]
theorem powersetAux'_nil : powersetAux' (@nil α) = [0] :=
  rfl
Powerset of Empty List is Singleton Zero Multiset
Informal description
The powerset of the empty list is the singleton multiset containing the empty multiset, i.e., $\text{powersetAux}'(\text{nil}) = \{0\}$.
Multiset.powersetAux'_cons theorem
(a : α) (l : List α) : powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)
Full source 
@[simp]
theorem powersetAux'_cons (a : α) (l : List α) :
    powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l) := by
  simp [powersetAux']
Recursive Construction of Multiset Powerset for Cons List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the powerset of the list $a :: l$ is equal to the concatenation of the powerset of $l$ with the list obtained by inserting $a$ into each multiset in the powerset of $l$. More precisely: $$\text{powersetAux'}(a :: l) = \text{powersetAux'}(l) \mathbin{+\kern-1.5ex+} \text{map} (\text{cons } a) (\text{powersetAux'}(l))$$
Multiset.powerset_aux'_perm theorem
{l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAux' l₁ ~ powersetAux' l₂
Full source 
theorem powerset_aux'_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAux'powersetAux' l₁ ~ powersetAux' l₂ := by
  induction p with
  | nil => simp
  | cons _ _ IH =>
    simp only [powersetAux'_cons]
    exact IH.append (IH.map _)
  | swap a b =>
    simp only [powersetAux'_cons, map_append, List.map_map, append_assoc]
    apply Perm.append_left
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Permutation Invariance of Multiset Powerset Construction
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the list of sub-multisets generated by `powersetAux'` from $l_1$ is a permutation of the list generated from $l_2$ (i.e., $\text{powersetAux'}(l_1) \sim \text{powersetAux'}(l_2)$).
Multiset.powersetAux_perm theorem
{l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAux l₁ ~ powersetAux l₂
Full source 
theorem powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetAuxpowersetAux l₁ ~ powersetAux l₂ :=
  powersetAux_perm_powersetAux'.trans <|
    (powerset_aux'_perm p).trans powersetAux_perm_powersetAux'.symm
Permutation Invariance of Multiset Powerset Construction via `powersetAux`
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the list of sub-multisets generated by `powersetAux` from $l_1$ is a permutation of the list generated from $l_2$ (i.e., $\text{powersetAux}(l_1) \sim \text{powersetAux}(l_2)$).
Multiset.powerset definition
(s : Multiset α) : Multiset (Multiset α)
Full source 
/-- The power set of a multiset. -/
def powerset (s : Multiset α) : Multiset (Multiset α) :=
  Quot.liftOn s
    (fun l => (powersetAux l : Multiset (Multiset α)))
    (fun _ _ h => Quot.sound (powersetAux_perm h))
Power set of a multiset
Informal description
The power set of a multiset $s$ is the multiset consisting of all sub-multisets of $s$. More precisely, given a multiset $s$ of elements of type $\alpha$, the power set is constructed by lifting the list operation `powersetAux` to multisets via the quotient construction. For any list $l$ representing $s$, `powersetAux l` generates a list of all sublists of $l$ converted to multisets, and this is then lifted to a multiset of multisets. The construction respects the equivalence relation on lists that defines multisets, ensuring the result is independent of the choice of representative list for $s$.
Multiset.powerset_coe theorem
(l : List α) : @powerset α l = ((sublists l).map (↑) : List (Multiset α))
Full source 
theorem powerset_coe (l : List α) : @powerset α l = ((sublists l).map (↑) : List (Multiset α)) :=
  congr_arg ((↑) : List (Multiset α) → Multiset (Multiset α)) powersetAux_eq_map_coe
Power Set of Multiset via Sublists
Informal description
For any list $l$ of elements of type $\alpha$, the power set of the multiset associated with $l$ is equal to the list obtained by mapping the canonical embedding from lists to multisets over all sublists of $l$. In other words, if $\uparrow$ denotes the canonical map from lists to multisets, then $\text{powerset}(l) = \text{map}(\uparrow, \text{sublists}(l))$.
Multiset.powerset_coe' theorem
(l : List α) : @powerset α l = ((sublists' l).map (↑) : List (Multiset α))
Full source 
@[simp]
theorem powerset_coe' (l : List α) : @powerset α l = ((sublists' l).map (↑) : List (Multiset α)) :=
  Quot.sound powersetAux_perm_powersetAux'
Power Set of Multiset via Sublists' Function
Informal description
For any list $l$ of elements of type $\alpha$, the power set of the multiset associated with $l$ is equal to the list obtained by mapping the canonical embedding from lists to multisets over all sublists of $l$ (computed via `sublists'`). In other words, if $\uparrow$ denotes the canonical map from lists to multisets, then $\text{powerset}(l) = \text{map}(\uparrow, \text{sublists'}(l))$.
Multiset.powerset_zero theorem
: @powerset α 0 = {0}
Full source 
@[simp]
theorem powerset_zero : @powerset α 0 = {0} :=
  rfl
Power Set of Empty Multiset is Singleton Zero
Informal description
The power set of the empty multiset $0$ is the singleton multiset $\{0\}$.
Multiset.powerset_cons theorem
(a : α) (s) : powerset (a ::ₘ s) = powerset s + map (cons a) (powerset s)
Full source 
@[simp]
theorem powerset_cons (a : α) (s) : powerset (a ::ₘ s) = powerset s + map (cons a) (powerset s) :=
  Quotient.inductionOn s fun l => by simp [Function.comp_def]
Powerset of Multiset Insertion: $\text{powerset}(a ::ₘ s) = \text{powerset}(s) + \text{map} (\text{cons } a) (\text{powerset}(s))$
Informal description
For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the powerset of the multiset obtained by inserting $a$ into $s$ (denoted $a ::ₘ s$) is equal to the sum of the powerset of $s$ and the multiset obtained by mapping the insertion of $a$ to each element of the powerset of $s$. More precisely: $$\text{powerset}(a ::ₘ s) = \text{powerset}(s) + \text{map} (\text{cons } a) (\text{powerset}(s))$$
Multiset.mem_powerset theorem
{s t : Multiset α} : s ∈ powerset t ↔ s ≤ t
Full source 
@[simp]
theorem mem_powerset {s t : Multiset α} : s ∈ powerset ts ∈ powerset t ↔ s ≤ t :=
  Quotient.inductionOn₂ s t <| by simp [Subperm, and_comm]
Characterization of Power Set Membership: $s \in \mathcal{P}(t) \leftrightarrow s \leq t$
Informal description
For any multisets $s$ and $t$ of elements of type $\alpha$, $s$ belongs to the power set of $t$ if and only if $s$ is a sub-multiset of $t$, i.e., $s \in \mathcal{P}(t) \leftrightarrow s \leq t$.
Multiset.map_single_le_powerset theorem
(s : Multiset α) : s.map singleton ≤ powerset s
Full source 
theorem map_single_le_powerset (s : Multiset α) : s.map singleton ≤ powerset s :=
  Quotient.inductionOn s fun l => by
    simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]
    show l.map (((↑) : List α → Multiset α) ∘ pure) <+~ (sublists l).map (↑)
    rw [← List.map_map]
    exact ((map_pure_sublist_sublists _).map _).subperm
Inclusion of Singleton Sub-multisets in Power Set: $\text{map}(\text{singleton}, s) \subseteq \text{powerset}(s)$
Informal description
For any multiset $s$ of elements of type $\alpha$, the multiset obtained by mapping the singleton operation over $s$ is a sub-multiset of the power set of $s$. In other words, the multiset of all singleton sub-multisets of $s$ is contained in the multiset of all sub-multisets of $s$. More formally: $$\text{map}(\text{singleton}, s) \subseteq \text{powerset}(s)$$
Multiset.card_powerset theorem
(s : Multiset α) : card (powerset s) = 2 ^ card s
Full source 
@[simp]
theorem card_powerset (s : Multiset α) : card (powerset s) = 2 ^ card s :=
  Quotient.inductionOn s <| by simp
Cardinality of Power Set of a Multiset: $|\mathcal{P}(s)| = 2^{|s|}$
Informal description
For any multiset $s$ of elements of type $\alpha$, the cardinality of its power set (the multiset of all sub-multisets of $s$) is equal to $2$ raised to the power of the cardinality of $s$, i.e., $$|\mathcal{P}(s)| = 2^{|s|}.$$
Multiset.revzip_powersetAux theorem
{l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux l)) : x.1 + x.2 = ↑l
Full source 
theorem revzip_powersetAux {l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux l)) : x.1 + x.2 = ↑l := by
  rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists _ _ _ h)
Sum of Sublist Multiset Pairs Equals Original Multiset
Informal description
For any list $l$ of elements of type $\alpha$, if $(s, t)$ is a pair in the reverse zip of the multiset of all sublists of $l$ (represented as multisets), then the sum of the multisets $s$ and $t$ equals the multiset corresponding to $l$. In other words, if $(s, t) \in \text{revzip}(\text{powersetAux}(l))$, then $s + t = \overline{l}$, where $\overline{l}$ denotes the multiset corresponding to the list $l$.
Multiset.revzip_powersetAux' theorem
{l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux' l)) : x.1 + x.2 = ↑l
Full source 
theorem revzip_powersetAux' {l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux' l)) :
    x.1 + x.2 = ↑l := by
  rw [revzip, powersetAux', ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists' _ _ _ h)
Sum of Sublist Multiset Pairs Equals Original Multiset
Informal description
For any list $l$ of elements of type $\alpha$, if $(s, t)$ is a pair in the reverse zip of the multiset of all sublists of $l$ (represented as multisets), then the sum of the multisets $s$ and $t$ equals the multiset corresponding to $l$. In other words, if $(s, t) \in \text{revzip}(\text{powersetAux'}(l))$, then $s + t = \overline{l}$, where $\overline{l}$ denotes the multiset corresponding to the list $l$.
Multiset.revzip_powersetAux_lemma theorem
{α : Type*} [DecidableEq α] (l : List α) {l' : List (Multiset α)} (H : ∀ ⦃x : _ × _⦄, x ∈ revzip l' → x.1 + x.2 = ↑l) : revzip l' = l'.map fun x => (x, (l : Multiset α) - x)
Full source 
theorem revzip_powersetAux_lemma {α : Type*} [DecidableEq α] (l : List α) {l' : List (Multiset α)}
    (H : ∀ ⦃x : _ × _⦄, x ∈ revzip l' → x.1 + x.2 = ↑l) :
    revzip l' = l'.map fun x => (x, (l : Multiset α) - x) := by
  have :
    Forall₂ (fun (p : MultisetMultiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
      ((revzip l').map Prod.fst) := by
    rw [forall₂_map_right_iff, forall₂_same]
    rintro ⟨s, t⟩ h
    dsimp
    rw [← H h, add_tsub_cancel_left]
  rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
  simpa using this
Decomposition of Reverse Zipped Powerset Multisets: $\text{revzip}(l') = \text{map} (x \mapsto (x, \overline{l} - x)) l'$
Informal description
Let $\alpha$ be a type with decidable equality, and let $l$ be a list of elements of type $\alpha$. Suppose $l'$ is a list of multisets over $\alpha$ such that for every pair $(s, t)$ in the reverse zip of $l'$, the sum $s + t$ equals the multiset corresponding to $l$. Then the reverse zip of $l'$ is equal to the list obtained by mapping each multiset $x$ in $l'$ to the pair $(x, \overline{l} - x)$, where $\overline{l}$ denotes the multiset corresponding to $l$.
Multiset.revzip_powersetAux_perm_aux' theorem
{l : List α} : revzip (powersetAux l) ~ revzip (powersetAux' l)
Full source 
theorem revzip_powersetAux_perm_aux' {l : List α} :
    revziprevzip (powersetAux l) ~ revzip (powersetAux' l) := by
  haveI := Classical.decEq α
  rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
  exact powersetAux_perm_powersetAux'.map _
Permutation of Reverse Zipped Powerset Multisets: $\text{revzip}(\text{powersetAux}(l)) \sim \text{revzip}(\text{powersetAux'}(l))$
Informal description
For any list $l$ of elements of type $\alpha$, the reverse zip of the multiset of all sublists of $l$ (computed via `powersetAux`) is a permutation of the reverse zip of the multiset of all sublists of $l$ (computed via `powersetAux'`). In other words, $\text{revzip}(\text{powersetAux}(l)) \sim \text{revzip}(\text{powersetAux'}(l))$, where $\sim$ denotes the permutation relation between lists.
Multiset.revzip_powersetAux_perm theorem
{l₁ l₂ : List α} (p : l₁ ~ l₂) : revzip (powersetAux l₁) ~ revzip (powersetAux l₂)
Full source 
theorem revzip_powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    revziprevzip (powersetAux l₁) ~ revzip (powersetAux l₂) := by
  haveI := Classical.decEq α
  simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
  exact (powersetAux_perm p).map _
Permutation Invariance of Reverse Zipped Powerset Multisets
Informal description
For any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the reverse zip of the multiset of all sublists of $l_1$ is a permutation of the reverse zip of the multiset of all sublists of $l_2$. In other words, $\text{revzip}(\text{powersetAux}(l_1)) \sim \text{revzip}(\text{powersetAux}(l_2))$, where $\sim$ denotes the permutation relation between lists.
Multiset.powersetCardAux definition
(n : ℕ) (l : List α) : List (Multiset α)
Full source 
/-- Helper function for `powersetCard`. Given a list `l`, `powersetCardAux n l` is the list
of sublists of length `n`, as multisets. -/
def powersetCardAux (n : ℕ) (l : List α) : List (Multiset α) :=
  sublistsLenAux n l (↑) []
List of length-`n` submultisets of a list
Informal description
Given a natural number `n` and a list `l` of elements of type `α`, the function `powersetCardAux` returns the list of all sublists of `l` of length `n`, represented as multisets. More precisely, for a multiset `s`, we have `s ∈ powersetCardAux n l` if and only if `s` is a submultiset of `l` (i.e., `s ≤ l`) and the cardinality of `s` is `n`.
Multiset.powersetCardAux_eq_map_coe theorem
{n} {l : List α} : powersetCardAux n l = (sublistsLen n l).map (↑)
Full source 
theorem powersetCardAux_eq_map_coe {n} {l : List α} :
    powersetCardAux n l = (sublistsLen n l).map (↑) := by
  rw [powersetCardAux, sublistsLenAux_eq, append_nil]
Equality of powersetCardAux and mapped sublistsLen via coercion
Informal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, the list of submultisets of $l$ with cardinality $n$ is equal to the list obtained by mapping the coercion function (from lists to multisets) over all sublists of $l$ with length $n$. In other words, the function `powersetCardAux n l` computes the same result as first generating all length-$n$ sublists of $l$ via `sublistsLen n l` and then converting each sublist to a multiset via the coercion function $\uparrow$.
Multiset.mem_powersetCardAux theorem
{n} {l : List α} {s} : s ∈ powersetCardAux n l ↔ s ≤ ↑l ∧ card s = n
Full source 
@[simp]
theorem mem_powersetCardAux {n} {l : List α} {s} : s ∈ powersetCardAux n ls ∈ powersetCardAux n l ↔ s ≤ ↑l ∧ card s = n :=
  Quotient.inductionOn s <| by
    simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen,
      coe_eq_coe, coe_le, Subperm, exists_prop, coe_card]
    exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩,
       fun ⟨⟨l₂, p, s⟩, e⟩ => ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩
Characterization of Submultisets in $\text{powersetCardAux}$
Informal description
For any natural number $n$, list $l$ of elements of type $\alpha$, and multiset $s$, the multiset $s$ belongs to the list $\text{powersetCardAux}\ n\ l$ if and only if $s$ is a submultiset of the multiset obtained from $l$ (i.e., $s \leq \uparrow l$) and the cardinality of $s$ is $n$.
Multiset.powersetCardAux_zero theorem
(l : List α) : powersetCardAux 0 l = [0]
Full source 
@[simp]
theorem powersetCardAux_zero (l : List α) : powersetCardAux 0 l = [0] := by
  simp [powersetCardAux_eq_map_coe]
Zero-cardinality submultisets are only the empty multiset
Informal description
For any list $l$ of elements of type $\alpha$, the list of submultisets of $l$ with cardinality $0$ is the singleton list containing the empty multiset, i.e., $\text{powersetCardAux}\ 0\ l = [0]$.
Multiset.powersetCardAux_nil theorem
(n : ℕ) : powersetCardAux (n + 1) (@nil α) = []
Full source 
@[simp]
theorem powersetCardAux_nil (n : ℕ) : powersetCardAux (n + 1) (@nil α) = [] :=
  rfl
Empty List Has No Nonempty Submultisets
Informal description
For any natural number $n$, the list of submultisets of length $n+1$ of the empty list is empty, i.e., $\text{powersetCardAux}(n+1, \text{nil}) = \text{nil}$.
Multiset.powersetCardAux_cons theorem
(n : ℕ) (a : α) (l : List α) : powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)
Full source 
@[simp]
theorem powersetCardAux_cons (n : ℕ) (a : α) (l : List α) :
    powersetCardAux (n + 1) (a :: l) =
      powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l) := by
  simp [powersetCardAux_eq_map_coe]
Recursive Construction of Submultisets of Length $n+1$ via Insertion
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and list $l$ of elements of type $\alpha$, the list of submultisets of length $n+1$ of the list $a :: l$ is equal to the concatenation of: 1. The list of all submultisets of length $n+1$ of $l$, and 2. The list obtained by inserting $a$ into each submultiset of length $n$ of $l$. In symbols: $$\text{powersetCardAux}(n+1, a :: l) = \text{powersetCardAux}(n+1, l) \mathbin{+\!\!+} \text{map}\ (\text{cons}\ a)\ (\text{powersetCardAux}\ n\ l)$$
Multiset.powersetCardAux_perm theorem
{n} {l₁ l₂ : List α} (p : l₁ ~ l₂) : powersetCardAux n l₁ ~ powersetCardAux n l₂
Full source 
theorem powersetCardAux_perm {n} {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    powersetCardAuxpowersetCardAux n l₁ ~ powersetCardAux n l₂ := by
  induction' n with n IHn generalizing l₁ l₂
  · simp
  induction p with
  | nil => rfl
  | cons _ p IH =>
    simp only [powersetCardAux_cons]
    exact IH.append ((IHn p).map _)
  | swap a b =>
    simp only [powersetCardAux_cons, append_assoc]
    apply Perm.append_left
    cases n
    · simp [Perm.swap]
    simp only [powersetCardAux_cons, map_append, List.map_map]
    rw [← append_assoc, ← append_assoc,
      (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)]
    exact perm_append_comm.append_right _
  | trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂
Permutation Invariance of Submultiset Lists: $\text{powersetCardAux}\ n\ l_1 \sim \text{powersetCardAux}\ n\ l_2$ when $l_1 \sim l_2$
Informal description
For any natural number $n$ and any two lists $l_1$ and $l_2$ of elements of type $\alpha$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the list of submultisets of length $n$ of $l_1$ is a permutation of the list of submultisets of length $n$ of $l_2$. In symbols: $$ l_1 \sim l_2 \implies \text{powersetCardAux}\ n\ l_1 \sim \text{powersetCardAux}\ n\ l_2 $$
Multiset.powersetCard definition
(n : ℕ) (s : Multiset α) : Multiset (Multiset α)
Full source 
/-- `powersetCard n s` is the multiset of all submultisets of `s` of length `n`. -/
def powersetCard (n : ℕ) (s : Multiset α) : Multiset (Multiset α) :=
  Quot.liftOn s (fun l => (powersetCardAux n l : Multiset (Multiset α))) fun _ _ h =>
    Quot.sound (powersetCardAux_perm h)
Multiset of submultisets with fixed cardinality
Informal description
For a natural number \( n \) and a multiset \( s \) of elements of type \( \alpha \), the function `powersetCard` returns the multiset of all submultisets of \( s \) with exactly \( n \) elements. More precisely, a multiset \( t \) is in `powersetCard n s` if and only if \( t \) is a submultiset of \( s \) (i.e., \( t \leq s \)) and the cardinality of \( t \) is \( n \).
Multiset.powersetCard_coe' theorem
(n) (l : List α) : @powersetCard α n l = powersetCardAux n l
Full source 
theorem powersetCard_coe' (n) (l : List α) : @powersetCard α n l = powersetCardAux n l :=
  rfl
Equality of `powersetCard` and `powersetCardAux` for lists
Informal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, the multiset of submultisets of $l$ with exactly $n$ elements (denoted `powersetCard n l`) is equal to the list of sublists of $l$ of length $n$ converted to a multiset (denoted `powersetCardAux n l`).
Multiset.powersetCard_coe theorem
(n) (l : List α) : @powersetCard α n l = ((sublistsLen n l).map (↑) : List (Multiset α))
Full source 
theorem powersetCard_coe (n) (l : List α) :
    @powersetCard α n l = ((sublistsLen n l).map (↑) : List (Multiset α)) :=
  congr_arg ((↑) : List (Multiset α) → Multiset (Multiset α)) powersetCardAux_eq_map_coe
Equality of powersetCard and mapped sublists via canonical embedding
Informal description
For any natural number $n$ and list $l$ of elements of type $\alpha$, the multiset of all submultisets of $l$ with exactly $n$ elements is equal to the list of all length-$n$ sublists of $l$ converted to multisets via the canonical embedding. In other words, $\text{powersetCard}_\alpha(n, l) = \{\![ t \mid t \in \text{sublistsLen}(n, l) \}\!}$, where $\{\![ \cdot \}\!}$ denotes the canonical embedding from lists to multisets.
Multiset.powersetCard_zero_left theorem
(s : Multiset α) : powersetCard 0 s = {0}
Full source 
@[simp]
theorem powersetCard_zero_left (s : Multiset α) : powersetCard 0 s = {0} :=
  Quotient.inductionOn s fun l => by simp [powersetCard_coe']
Zero-cardinality submultisets are the empty multiset
Informal description
For any multiset $s$ of elements of type $\alpha$, the multiset of all submultisets of $s$ with cardinality $0$ is the singleton multiset containing only the empty multiset, i.e., $\text{powersetCard}(0, s) = \{0\}$.
Multiset.powersetCard_zero_right theorem
(n : ℕ) : @powersetCard α (n + 1) 0 = 0
Full source 
theorem powersetCard_zero_right (n : ℕ) : @powersetCard α (n + 1) 0 = 0 :=
  rfl
Empty Multiset Has No Submultisets of Positive Cardinality
Informal description
For any natural number $n$, the multiset of submultisets with exactly $n+1$ elements of the empty multiset $0$ is itself the empty multiset $0$. In other words, $\text{powersetCard}(n+1, 0) = 0$.
Multiset.powersetCard_cons theorem
(n : ℕ) (a : α) (s) : powersetCard (n + 1) (a ::ₘ s) = powersetCard (n + 1) s + map (cons a) (powersetCard n s)
Full source 
@[simp]
theorem powersetCard_cons (n : ℕ) (a : α) (s) :
    powersetCard (n + 1) (a ::ₘ s) = powersetCard (n + 1) s + map (cons a) (powersetCard n s) :=
  Quotient.inductionOn s fun l => by simp [powersetCard_coe']
Recursive Construction of Submultisets with Fixed Cardinality via Insertion
Informal description
For any natural number $n$, element $a$ of type $\alpha$, and multiset $s$ over $\alpha$, the multiset of submultisets with exactly $n+1$ elements of the multiset $a ::ₘ s$ is equal to the sum of: 1. The multiset of submultisets with exactly $n+1$ elements of $s$, and 2. The multiset obtained by inserting $a$ into each submultiset with exactly $n$ elements of $s$. In symbols: $$\text{powersetCard}(n+1, a ::ₘ s) = \text{powersetCard}(n+1, s) + \text{map}\ (\text{cons}\ a)\ (\text{powersetCard}\ n\ s)$$
Multiset.powersetCard_one theorem
(s : Multiset α) : powersetCard 1 s = s.map singleton
Full source 
theorem powersetCard_one (s : Multiset α) : powersetCard 1 s = s.map singleton :=
  Quotient.inductionOn s fun l ↦ by
    simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]
Submultisets of Cardinality One are Singletons
Informal description
For any multiset $s$ of elements of type $\alpha$, the multiset of all submultisets of $s$ with exactly one element is equal to the multiset obtained by mapping each element $a \in s$ to the singleton multiset $\{a\}$.
Multiset.mem_powersetCard theorem
{n : ℕ} {s t : Multiset α} : s ∈ powersetCard n t ↔ s ≤ t ∧ card s = n
Full source 
@[simp]
theorem mem_powersetCard {n : ℕ} {s t : Multiset α} : s ∈ powersetCard n ts ∈ powersetCard n t ↔ s ≤ t ∧ card s = n :=
  Quotient.inductionOn t fun l => by simp [powersetCard_coe']
Characterization of Submultisets with Fixed Cardinality
Informal description
For any natural number $n$ and multisets $s$ and $t$ of elements of type $\alpha$, the submultiset $s$ belongs to the multiset of submultisets of $t$ with cardinality $n$ if and only if $s$ is a submultiset of $t$ (i.e., $s \leq t$) and the cardinality of $s$ is equal to $n$. In symbols: $s \in \text{powersetCard}_n(t) \leftrightarrow s \leq t \land |s| = n$.
Multiset.card_powersetCard theorem
(n : ℕ) (s : Multiset α) : card (powersetCard n s) = Nat.choose (card s) n
Full source 
@[simp]
theorem card_powersetCard (n : ℕ) (s : Multiset α) :
    card (powersetCard n s) = Nat.choose (card s) n :=
  Quotient.inductionOn s <| by simp [powersetCard_coe]
Cardinality of Fixed-Size Submultisets: $\text{card}(\text{powersetCard}_n(s)) = \binom{|s|}{n}$
Informal description
For any natural number $n$ and multiset $s$ of elements of type $\alpha$, the number of submultisets of $s$ with exactly $n$ elements is equal to the binomial coefficient $\binom{|s|}{n}$, where $|s|$ denotes the cardinality of $s$.
Multiset.powersetCard_le_powerset theorem
(n : ℕ) (s : Multiset α) : powersetCard n s ≤ powerset s
Full source 
theorem powersetCard_le_powerset (n : ℕ) (s : Multiset α) : powersetCard n s ≤ powerset s :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, powersetCard_coe, powerset_coe', coe_le]
    exact ((sublistsLen_sublist_sublists' _ _).map _).subperm
Inclusion of Fixed-Size Submultisets in Power Set: $\text{powersetCard}_n(s) \subseteq \text{powerset}(s)$
Informal description
For any natural number $n$ and multiset $s$ of elements of type $\alpha$, the multiset of all submultisets of $s$ with exactly $n$ elements is a submultiset of the power set of $s$. In symbols: $\text{powersetCard}_n(s) \leq \text{powerset}(s)$.
Multiset.powersetCard_mono theorem
(n : ℕ) {s t : Multiset α} (h : s ≤ t) : powersetCard n s ≤ powersetCard n t
Full source 
theorem powersetCard_mono (n : ℕ) {s t : Multiset α} (h : s ≤ t) :
    powersetCard n s ≤ powersetCard n t :=
  leInductionOn h fun {l₁ l₂} h => by
    simp only [powersetCard_coe, coe_le]
    exact ((sublistsLen_sublist_of_sublist _ h).map _).subperm
Monotonicity of Fixed-Cardinality Submultisets with Respect to Submultiset Relation
Informal description
For any natural number $n$ and multisets $s, t$ of elements of type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then the multiset of all submultisets of $s$ with exactly $n$ elements is a submultiset of the multiset of all submultisets of $t$ with exactly $n$ elements.
Multiset.powersetCard_eq_empty theorem
{α : Type*} (n : ℕ) {s : Multiset α} (h : card s < n) : powersetCard n s = 0
Full source 
@[simp]
theorem powersetCard_eq_empty {α : Type*} (n : ℕ) {s : Multiset α} (h : card s < n) :
    powersetCard n s = 0 :=
  card_eq_zero.mp (Nat.choose_eq_zero_of_lt h ▸ card_powersetCard _ _)
Vanishing of Fixed-Size Submultisets When $|s| < n$
Informal description
For any natural number $n$ and multiset $s$ of elements of type $\alpha$, if the cardinality of $s$ is less than $n$ (i.e., $|s| < n$), then the multiset of all submultisets of $s$ with exactly $n$ elements is empty, i.e., $\text{powersetCard}_n(s) = 0$.
Multiset.powersetCard_card_add theorem
(s : Multiset α) {i : ℕ} (hi : 0 < i) : s.powersetCard (card s + i) = 0
Full source 
@[simp]
theorem powersetCard_card_add (s : Multiset α) {i : ℕ} (hi : 0 < i) :
    s.powersetCard (card s + i) = 0 :=
  powersetCard_eq_empty _ (Nat.lt_add_of_pos_right hi)
Vanishing of Submultisets with Cardinality Exceeding $|s|$
Informal description
For any multiset $s$ of elements of type $\alpha$ and any positive natural number $i$, the multiset of all submultisets of $s$ with cardinality $|s| + i$ is empty, i.e., $\text{powersetCard}_{|s| + i}(s) = 0$.
Multiset.powersetCard_map theorem
{β : Type*} (f : α → β) (n : ℕ) (s : Multiset α) : powersetCard n (s.map f) = (powersetCard n s).map (map f)
Full source 
theorem powersetCard_map {β : Type*} (f : α → β) (n : ℕ) (s : Multiset α) :
    powersetCard n (s.map f) = (powersetCard n s).map (map f) := by
  induction' s using Multiset.induction with t s ih generalizing n
  · cases n <;> simp [powersetCard_zero_left, powersetCard_zero_right]
  · cases n <;> simp [ih, map_comp_cons]
Mapping Preserves Fixed-Size Submultisets: $\text{powersetCard}_n(s.map\ f) = (\text{powersetCard}_n\ s).map\ (map\ f)$
Informal description
For any function $f : \alpha \to \beta$, natural number $n$, and multiset $s$ over $\alpha$, the multiset of submultisets with exactly $n$ elements of the image multiset $s.map\ f$ is equal to the image under $map\ f$ of the multiset of submultisets with exactly $n$ elements of $s$. In symbols: $$\text{powersetCard}_n(s.map\ f) = (\text{powersetCard}_n\ s).map\ (map\ f)$$
Multiset.pairwise_disjoint_powersetCard theorem
(s : Multiset α) : _root_.Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j)
Full source 
theorem pairwise_disjoint_powersetCard (s : Multiset α) :
    _root_.Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j) :=
  fun _ _ h ↦ disjoint_left.mpr fun hi hj ↦
    h ((Multiset.mem_powersetCard.mp hi).2.symm.trans (Multiset.mem_powersetCard.mp hj).2)
Pairwise Disjointness of Submultisets with Different Cardinalities
Informal description
For any multiset $s$ of elements of type $\alpha$, the collection of submultisets with fixed cardinalities is pairwise disjoint. That is, for any two distinct natural numbers $i$ and $j$, the multiset of submultisets of $s$ with cardinality $i$ is disjoint from the multiset of submultisets of $s$ with cardinality $j$. In symbols: for all $i \neq j$, $\text{powersetCard}_i(s) \cap \text{powersetCard}_j(s) = \emptyset$.
Multiset.bind_powerset_len theorem
{α : Type*} (S : Multiset α) : (bind (Multiset.range (card S + 1)) fun k => S.powersetCard k) = S.powerset
Full source 
theorem bind_powerset_len {α : Type*} (S : Multiset α) :
    (bind (Multiset.range (card S + 1)) fun k => S.powersetCard k) = S.powerset := by
  induction S using Quotient.inductionOn
  simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
    ← List.map_flatMap, coe_card]
  exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)
Decomposition of Multiset Power Set by Cardinality
Informal description
For any multiset $S$ over a type $\alpha$, the union of all submultisets of $S$ with cardinalities ranging from $0$ to the cardinality of $S$ is equal to the power set of $S$. In symbols: $$\bigcup_{k=0}^{|S|} \text{powersetCard}_k(S) = \text{powerset}(S)$$
Multiset.nodup_powerset theorem
{s : Multiset α} : Nodup (powerset s) ↔ Nodup s
Full source 
@[simp]
theorem nodup_powerset {s : Multiset α} : NodupNodup (powerset s) ↔ Nodup s :=
  ⟨fun h => (nodup_of_le (map_single_le_powerset _) h).of_map _,
    Quotient.inductionOn s fun l h => by
      simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
      refine (nodup_sublists'.2 h).map_on ?_
      exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)⟩
Distinctness of Power Set is Equivalent to Distinctness of Original Multiset
Informal description
For any multiset $s$ of elements of type $\alpha$, the power set of $s$ (the multiset of all submultisets of $s$) has no duplicate elements if and only if $s$ itself has no duplicate elements.
Multiset.Nodup.powersetCard theorem
{n : ℕ} {s : Multiset α} (h : Nodup s) : Nodup (powersetCard n s)
Full source 
protected theorem Nodup.powersetCard {n : ℕ} {s : Multiset α} (h : Nodup s) :
    Nodup (powersetCard n s) :=
  nodup_of_le (powersetCard_le_powerset _ _) (nodup_powerset.2 h)
Distinctness of Fixed-Size Submultisets of a Distinct Multiset
Informal description
For any natural number $n$ and any multiset $s$ of elements of type $\alpha$, if $s$ has no duplicate elements, then the multiset of all submultisets of $s$ with exactly $n$ elements also has no duplicate elements.