mathlib documentation

data.multiset.powerset

The powerset of a multiset

powerset

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

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} :
list αlist (multiset α)

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 α} :

theorem multiset.powerset_aux_perm {α : Type u_1} {l₁ l₂ : list α} :

def multiset.powerset {α : Type u_1} :

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} :

@[simp]
theorem multiset.powerset_cons {α : Type u_1} (a : α) (s : multiset α) :

@[simp]
theorem multiset.mem_powerset {α : Type u_1} {s t : multiset α} :

theorem multiset.map_single_le_powerset {α : Type u_1} (s : multiset α) :
multiset.map (λ (a : α), a ::ₘ 0) s s.powerset

@[simp]
theorem multiset.card_powerset {α : Type u_1} (s : multiset α) :

theorem multiset.revzip_powerset_aux {α : Type u_1} {l : list α} ⦃x : multiset α × multiset α :

theorem multiset.revzip_powerset_aux' {α : Type u_1} {l : list α} ⦃x : multiset α × multiset α :

theorem multiset.revzip_powerset_aux_lemma {α : Type u_1} [decidable_eq α] (l : list α) {l' : list (multiset α)} :
(∀ ⦃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 α} :

powerset_len

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

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 α} :

def multiset.powerset_len {α : Type u_1} :
multiset αmultiset (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 α) :

@[simp]
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.card_powerset_len {α : Type u_1} (n : ) (s : multiset α) :

theorem multiset.powerset_len_le_powerset {α : Type u_1} (n : ) (s : multiset α) :

theorem multiset.powerset_len_mono {α : Type u_1} (n : ) {s t : multiset α} :