# 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
Instances For
theorem Multiset.powersetAux_eq_map_coe {α : Type u_1} {l : List α} :
= List.map Multiset.ofList l.sublists
@[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
Instances For
theorem Multiset.powersetAux_perm_powersetAux' {α : Type u_1} {l : List α} :
.Perm
@[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₁.Perm l₂) :
.Perm
theorem Multiset.powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
().Perm ()
def Multiset.powerset {α : Type u_1} (s : ) :

The power set of a multiset.

Equations
Instances For
theorem Multiset.powerset_coe {α : Type u_1} (l : List α) :
(l).powerset = (List.map Multiset.ofList l.sublists)
@[simp]
theorem Multiset.powerset_coe' {α : Type u_1} (l : List α) :
(l).powerset = (List.map Multiset.ofList l.sublists')
@[simp]
theorem Multiset.powerset_zero {α : Type u_1} :
= {0}
@[simp]
theorem Multiset.powerset_cons {α : Type u_1} (a : α) (s : ) :
(a ::ₘ s).powerset = s.powerset + Multiset.map () s.powerset
@[simp]
theorem Multiset.mem_powerset {α : Type u_1} {s : } {t : } :
s t.powerset s t
theorem Multiset.map_single_le_powerset {α : Type u_1} (s : ) :
Multiset.map singleton s s.powerset
@[simp]
theorem Multiset.card_powerset {α : Type u_1} (s : ) :
Multiset.card s.powerset = 2 ^ Multiset.card s
theorem Multiset.revzip_powersetAux {α : Type u_1} {l : List α} ⦃x : (h : x .revzip) :
x.1 + x.2 = l
theorem Multiset.revzip_powersetAux' {α : Type u_1} {l : List α} ⦃x : (h : x .revzip) :
x.1 + x.2 = l
theorem Multiset.revzip_powersetAux_lemma {α : Type u_2} [] (l : List α) {l' : List ()} (H : ∀ ⦃x : ⦄, x l'.revzipx.1 + x.2 = l) :
l'.revzip = List.map (fun (x : ) => (x, l - x)) l'
theorem Multiset.revzip_powersetAux_perm_aux' {α : Type u_1} {l : List α} :
.revzip.Perm .revzip
theorem Multiset.revzip_powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
().revzip.Perm ().revzip

### powersetCard #

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

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

Equations
Instances For
theorem Multiset.powersetCardAux_eq_map_coe {α : Type u_1} {n : } {l : List α} :
= List.map Multiset.ofList ()
@[simp]
theorem Multiset.mem_powersetCardAux {α : Type u_1} {n : } {l : List α} {s : } :
s l Multiset.card s = n
@[simp]
theorem Multiset.powersetCardAux_zero {α : Type u_1} (l : List α) :
= [0]
@[simp]
theorem Multiset.powersetCardAux_nil {α : Type u_1} (n : ) :
@[simp]
theorem Multiset.powersetCardAux_cons {α : Type u_1} (n : ) (a : α) (l : List α) :
theorem Multiset.powersetCardAux_perm {α : Type u_1} {n : } {l₁ : List α} {l₂ : List α} (p : l₁.Perm l₂) :
().Perm ()
def Multiset.powersetCard {α : Type u_1} (n : ) (s : ) :

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

Equations
Instances For
theorem Multiset.powersetCard_coe' {α : Type u_1} (n : ) (l : List α) :
= ()
theorem Multiset.powersetCard_coe {α : Type u_1} (n : ) (l : List α) :
= (List.map Multiset.ofList ())
@[simp]
theorem Multiset.powersetCard_zero_left {α : Type u_1} (s : ) :
= {0}
@[simp]
theorem Multiset.powersetCard_cons {α : Type u_1} (n : ) (a : α) (s : ) :
theorem Multiset.powersetCard_one {α : Type u_1} (s : ) :
= Multiset.map singleton s
@[simp]
theorem Multiset.mem_powersetCard {α : Type u_1} {n : } {s : } {t : } :
s t Multiset.card s = n
@[simp]
theorem Multiset.card_powersetCard {α : Type u_1} (n : ) (s : ) :
Multiset.card () = (Multiset.card s).choose n
theorem Multiset.powersetCard_le_powerset {α : Type u_1} (n : ) (s : ) :
s.powerset
theorem Multiset.powersetCard_mono {α : Type u_1} (n : ) {s : } {t : } (h : s t) :
@[simp]
theorem Multiset.powersetCard_eq_empty {α : Type u_2} (n : ) {s : } (h : Multiset.card s < n) :
@[simp]
theorem Multiset.powersetCard_card_add {α : Type u_1} (s : ) {i : } (hi : 0 < i) :
Multiset.powersetCard (Multiset.card s + i) s = 0
theorem Multiset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : αβ) (n : ) (s : ) :
=
theorem Multiset.pairwise_disjoint_powersetCard {α : Type u_1} (s : ) :
Pairwise fun (i j : ) => ().Disjoint ()
theorem Multiset.bind_powerset_len {α : Type u_2} (S : ) :
((Multiset.range (Multiset.card S + 1)).bind fun (k : ) => ) = S.powerset
@[simp]
theorem Multiset.nodup_powerset {α : Type u_1} {s : } :
s.powerset.Nodup s.Nodup
theorem Multiset.Nodup.powerset {α : Type u_1} {s : } :
s.Nodups.powerset.Nodup

Alias of the reverse direction of Multiset.nodup_powerset.

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

Alias of the forward direction of Multiset.nodup_powerset.

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