# Documentation

Mathlib.Data.Multiset.Powerset

# The powerset of a multiset #

### powerset #

def Multiset.powersetAux {α : Type u_1} (l : List α) :
List ()

A helper function for the powerset of a multiset. Given a list l, returns a list of sublists of l as multisets.

Equations
theorem Multiset.powersetAux_eq_map_coe {α : Type u_1} {l : List α} :
= List.map Multiset.ofList ()
@[simp]
theorem Multiset.mem_powersetAux {α : Type u_1} {l : List α} {s : } :
s l
def Multiset.powersetAux' {α : Type u_1} (l : List α) :
List ()

Helper function for the powerset of a multiset. Given a list l, returns a list of sublists of l (using sublists'), as multisets.

Equations
@[simp]
theorem Multiset.powersetAux'_nil {α : Type u_1} :
= [0]
@[simp]
theorem Multiset.powersetAux'_cons {α : Type u_1} (a : α) (l : List α) :
theorem Multiset.powerset_aux'_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
theorem Multiset.powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
def Multiset.powerset {α : Type u_1} (s : ) :

The power set of a multiset.

Equations
• One or more equations did not get rendered due to their size.
theorem Multiset.powerset_coe {α : Type u_1} (l : List α) :
= ↑(List.map Multiset.ofList ())
@[simp]
theorem Multiset.powerset_coe' {α : Type u_1} (l : List α) :
= ↑(List.map Multiset.ofList ())
@[simp]
theorem Multiset.powerset_zero {α : Type u_1} :
= {0}
@[simp]
theorem Multiset.powerset_cons {α : Type u_1} (a : α) (s : ) :
@[simp]
theorem Multiset.mem_powerset {α : Type u_1} {s : } {t : } :
s t
theorem Multiset.map_single_le_powerset {α : Type u_1} (s : ) :
Multiset.map singleton s
@[simp]
theorem Multiset.card_powerset {α : Type u_1} (s : ) :
Multiset.card () = 2 ^ Multiset.card s
theorem Multiset.revzip_powersetAux {α : Type u_1} {l : List α} ⦃x : (h : ) :
x.fst + x.snd = l
theorem Multiset.revzip_powersetAux' {α : Type u_1} {l : List α} ⦃x : (h : ) :
x.fst + x.snd = l
theorem Multiset.revzip_powersetAux_lemma {α : Type u} [inst : ] (l : List α) {l' : List ()} (H : ∀ ⦃x : ⦄, x x.fst + x.snd = l) :
= List.map (fun x => (x, l - x)) l'
theorem Multiset.revzip_powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :

### powersetLen #

def Multiset.powersetLenAux {α : Type u_1} (n : ) (l : List α) :
List ()

Helper function for powersetLen. Given a list l, powersetLenAux n l is the list of sublists of length n, as multisets.

Equations
theorem Multiset.powersetLenAux_eq_map_coe {α : Type u_1} {n : } {l : List α} :
= List.map Multiset.ofList ()
@[simp]
theorem Multiset.mem_powersetLenAux {α : Type u_1} {n : } {l : List α} {s : } :
s l Multiset.card s = n
@[simp]
theorem Multiset.powersetLenAux_zero {α : Type u_1} (l : List α) :
= [0]
@[simp]
theorem Multiset.powersetLenAux_nil {α : Type u_1} (n : ) :
@[simp]
theorem Multiset.powersetLenAux_cons {α : Type u_1} (n : ) (a : α) (l : List α) :
theorem Multiset.powersetLenAux_perm {α : Type u_1} {n : } {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) :
def Multiset.powersetLen {α : Type u_1} (n : ) (s : ) :

powersetLen n s is the multiset of all submultisets of s of length n.

Equations
• One or more equations did not get rendered due to their size.
theorem Multiset.powersetLen_coe' {α : Type u_1} (n : ) (l : List α) :
= ↑()
theorem Multiset.powersetLen_coe {α : Type u_1} (n : ) (l : List α) :
= ↑(List.map Multiset.ofList ())
@[simp]
theorem Multiset.powersetLen_zero_left {α : Type u_1} (s : ) :
= {0}
@[simp]
theorem Multiset.powersetLen_cons {α : Type u_1} (n : ) (a : α) (s : ) :
@[simp]
theorem Multiset.mem_powersetLen {α : Type u_1} {n : } {s : } {t : } :
s t Multiset.card s = n
@[simp]
theorem Multiset.card_powersetLen {α : Type u_1} (n : ) (s : ) :
Multiset.card () = Nat.choose (Multiset.card s) n
theorem Multiset.powersetLen_le_powerset {α : Type u_1} (n : ) (s : ) :
theorem Multiset.powersetLen_mono {α : Type u_1} (n : ) {s : } {t : } (h : s t) :
@[simp]
theorem Multiset.powersetLen_empty {α : Type u_1} (n : ) {s : } (h : Multiset.card s < n) :
@[simp]
theorem Multiset.powersetLen_card_add {α : Type u_1} (s : ) {i : } (hi : 0 < i) :
Multiset.powersetLen (Multiset.card s + i) s = 0
theorem Multiset.powersetLen_map {α : Type u_2} {β : Type u_1} (f : αβ) (n : ) (s : ) :
theorem Multiset.pairwise_disjoint_powersetLen {α : Type u_1} (s : ) :
Pairwise fun i j =>
theorem Multiset.bind_powerset_len {α : Type u_1} (S : ) :
(Multiset.bind (Multiset.range (Multiset.card S + 1)) fun k => ) =
@[simp]
theorem Multiset.nodup_powerset {α : Type u_1} {s : } :
theorem Multiset.Nodup.ofPowerset {α : Type u_1} {s : } :

Alias of the forward direction of Multiset.nodup_powerset.

theorem Multiset.Nodup.powerset {α : Type u_1} {s : } :

Alias of the reverse direction of Multiset.nodup_powerset.

theorem Multiset.Nodup.powersetLen {α : Type u_1} {n : } {s : } (h : ) :