mathlib documentation

data.multiset.powerset

The powerset of a multiset #

powerset #

def multiset.powerset_aux {α : Type u_1} (l : list α) :

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

Equations
@[simp]
theorem multiset.mem_powerset_aux {α : Type u_1} {l : list α} {s : multiset α} :
def multiset.powerset_aux' {α : Type u_1} (l : 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.powerset_aux'_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
theorem multiset.powerset_aux_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
def multiset.powerset {α : Type u_1} (s : multiset α) :

The power set of a multiset.

Equations
theorem multiset.powerset_coe {α : Type u_1} (l : list α) :
@[simp]
theorem multiset.powerset_coe' {α : Type u_1} (l : list α) :
@[simp]
theorem multiset.powerset_zero {α : Type u_1} :
0.powerset = {0}
@[simp]
theorem multiset.powerset_cons {α : Type u_1} (a : α) (s : multiset α) :
@[simp]
theorem multiset.mem_powerset {α : Type u_1} {s t : multiset α} :
@[simp]
theorem multiset.card_powerset {α : Type u_1} (s : multiset α) :
theorem multiset.revzip_powerset_aux {α : Type u_1} {l : list α} ⦃x : multiset α × multiset α (h : x (multiset.powerset_aux l).revzip) :
x.fst + x.snd = l
theorem multiset.revzip_powerset_aux' {α : Type u_1} {l : list α} ⦃x : multiset α × multiset α (h : x (multiset.powerset_aux' l).revzip) :
x.fst + x.snd = l
theorem multiset.revzip_powerset_aux_lemma {α : Type u_1} [decidable_eq α] (l : list α) {l' : list (multiset α)} (H : ∀ ⦃x : multiset α × multiset α⦄, x l'.revzipx.fst + x.snd = l) :
l'.revzip = list.map (λ (x : multiset α), (x, l - x)) l'
theorem multiset.revzip_powerset_aux_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :

powerset_len #

def multiset.powerset_len_aux {α : Type u_1} (n : ) (l : list α) :

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

Equations
@[simp]
theorem multiset.mem_powerset_len_aux {α : Type u_1} {n : } {l : list α} {s : multiset α} :
@[simp]
theorem multiset.powerset_len_aux_zero {α : Type u_1} (l : list α) :
@[simp]
@[simp]
theorem multiset.powerset_len_aux_cons {α : Type u_1} (n : ) (a : α) (l : list α) :
theorem multiset.powerset_len_aux_perm {α : Type u_1} {n : } {l₁ l₂ : list α} (p : l₁ ~ l₂) :
def multiset.powerset_len {α : Type u_1} (n : ) (s : multiset α) :

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

Equations
theorem multiset.powerset_len_coe {α : Type u_1} (n : ) (l : list α) :
@[simp]
theorem multiset.powerset_len_zero_left {α : Type u_1} (s : multiset α) :
theorem multiset.powerset_len_zero_right {α : Type u_1} (n : ) :
@[simp]
theorem multiset.powerset_len_cons {α : Type u_1} (n : ) (a : α) (s : multiset α) :
@[simp]
theorem multiset.mem_powerset_len {α : Type u_1} {n : } {s t : multiset α} :
@[simp]
theorem multiset.powerset_len_le_powerset {α : Type u_1} (n : ) (s : multiset α) :
theorem multiset.powerset_len_mono {α : Type u_1} (n : ) {s t : multiset α} (h : s t) :
@[simp]
theorem multiset.powerset_len_empty {α : Type u_1} (n : ) {s : multiset α} (h : multiset.card s < n) :
@[simp]
theorem multiset.powerset_len_card_add {α : Type u_1} (s : multiset α) {i : } (hi : 0 < i) :
theorem multiset.powerset_len_map {α : Type u_1} {β : Type u_2} (f : α → β) (n : ) (s : multiset α) :
theorem multiset.disjoint_powerset_len {α : Type u_1} (s : multiset α) {i j : } (h : i j) :
theorem multiset.bind_powerset_len {α : Type u_1} (S : multiset α) :