The powerset of a multiset

powerset

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

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

Equations

• Multiset.powersetAux l = List.map Multiset.ofList (List.sublists l)

theorem Multiset.powersetAux_eq_map_coe {α : Type u_1} {l : List α} : Multiset.powersetAux l = List.map Multiset.ofList (List.sublists l)

@[simp]

theorem Multiset.mem_powersetAux {α : Type u_1} {l : List α} {s : Multiset α} : s ∈ Multiset.powersetAux l ↔ s ≤ ↑l

def Multiset.powersetAux' {α : Type u_1} (l : 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

• Multiset.powersetAux' l = List.map Multiset.ofList (List.sublists' l)

theorem Multiset.powersetAux_perm_powersetAux' {α : Type u_1} {l : List α} : Multiset.powersetAux l ~ Multiset.powersetAux' l

@[simp]

theorem Multiset.powersetAux'_nil {α : Type u_1} : Multiset.powersetAux' [] = [0]

@[simp]

theorem Multiset.powersetAux'_cons {α : Type u_1} (a : α) (l : List α) : Multiset.powersetAux' (a :: l) = Multiset.powersetAux' l ++ List.map (Multiset.cons a) (Multiset.powersetAux' l)

theorem Multiset.powerset_aux'_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : Multiset.powersetAux' l₁ ~ Multiset.powersetAux' l₂

theorem Multiset.powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : Multiset.powersetAux l₁ ~ Multiset.powersetAux l₂

def Multiset.powerset {α : Type u_1} (s : Multiset α) : Multiset (Multiset α)

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 α) : Multiset.powerset ↑l = ↑(List.map Multiset.ofList (List.sublists l))

@[simp]

theorem Multiset.powerset_coe' {α : Type u_1} (l : List α) : Multiset.powerset ↑l = ↑(List.map Multiset.ofList (List.sublists' l))

@[simp]

theorem Multiset.powerset_zero {α : Type u_1} : Multiset.powerset 0 = {0}

@[simp]

theorem Multiset.powerset_cons {α : Type u_1} (a : α) (s : Multiset α) : Multiset.powerset (a ::ₘ s) = Multiset.powerset s + Multiset.map (Multiset.cons a) (Multiset.powerset s)

@[simp]

theorem Multiset.mem_powerset {α : Type u_1} {s : Multiset α} {t : Multiset α} : s ∈ Multiset.powerset t ↔ s ≤ t

theorem Multiset.map_single_le_powerset {α : Type u_1} (s : Multiset α) : Multiset.map singleton s ≤ Multiset.powerset s

@[simp]

theorem Multiset.card_powerset {α : Type u_1} (s : Multiset α) : ↑Multiset.card (Multiset.powerset s) = 2 ^ ↑Multiset.card s

theorem Multiset.revzip_powersetAux {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α⦄ (h : x ∈ List.revzip (Multiset.powersetAux l)) : x.fst + x.snd = ↑l

theorem Multiset.revzip_powersetAux' {α : Type u_1} {l : List α} ⦃x : Multiset α × Multiset α⦄ (h : x ∈ List.revzip (Multiset.powersetAux' l)) : x.fst + x.snd = ↑l

theorem Multiset.revzip_powersetAux_lemma {α : Type u} [DecidableEq α] (l : List α) {l' : List (Multiset α)} (H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ List.revzip l' → x.fst + x.snd = ↑l) : List.revzip l' = List.map (fun x => (x, ↑l - x)) l'

theorem Multiset.revzip_powersetAux_perm_aux' {α : Type u_1} {l : List α} : List.revzip (Multiset.powersetAux l) ~ List.revzip (Multiset.powersetAux' l)

theorem Multiset.revzip_powersetAux_perm {α : Type u_1} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : List.revzip (Multiset.powersetAux l₁) ~ List.revzip (Multiset.powersetAux l₂)

powersetLen

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

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

Equations

• Multiset.powersetLenAux n l = List.sublistsLenAux n l Multiset.ofList []

theorem Multiset.powersetLenAux_eq_map_coe {α : Type u_1} {n : ℕ} {l : List α} : Multiset.powersetLenAux n l = List.map Multiset.ofList (List.sublistsLen n l)

@[simp]

theorem Multiset.mem_powersetLenAux {α : Type u_1} {n : ℕ} {l : List α} {s : Multiset α} : s ∈ Multiset.powersetLenAux n l ↔ s ≤ ↑l ∧ ↑Multiset.card s = n

@[simp]

theorem Multiset.powersetLenAux_zero {α : Type u_1} (l : List α) : Multiset.powersetLenAux 0 l = [0]

@[simp]

theorem Multiset.powersetLenAux_nil {α : Type u_1} (n : ℕ) : Multiset.powersetLenAux (n + 1) [] = []

@[simp]

theorem Multiset.powersetLenAux_cons {α : Type u_1} (n : ℕ) (a : α) (l : List α) : Multiset.powersetLenAux (n + 1) (a :: l) = Multiset.powersetLenAux (n + 1) l ++ List.map (Multiset.cons a) (Multiset.powersetLenAux n l)

theorem Multiset.powersetLenAux_perm {α : Type u_1} {n : ℕ} {l₁ : List α} {l₂ : List α} (p : l₁ ~ l₂) : Multiset.powersetLenAux n l₁ ~ Multiset.powersetLenAux n l₂

def Multiset.powersetLen {α : Type u_1} (n : ℕ) (s : Multiset α) : Multiset (Multiset α)

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 α) : Multiset.powersetLen n ↑l = ↑(Multiset.powersetLenAux n l)

theorem Multiset.powersetLen_coe {α : Type u_1} (n : ℕ) (l : List α) : Multiset.powersetLen n ↑l = ↑(List.map Multiset.ofList (List.sublistsLen n l))

@[simp]

theorem Multiset.powersetLen_zero_left {α : Type u_1} (s : Multiset α) : Multiset.powersetLen 0 s = {0}

theorem Multiset.powersetLen_zero_right {α : Type u_1} (n : ℕ) : Multiset.powersetLen (n + 1) 0 = 0

@[simp]

theorem Multiset.powersetLen_cons {α : Type u_1} (n : ℕ) (a : α) (s : Multiset α) : Multiset.powersetLen (n + 1) (a ::ₘ s) = Multiset.powersetLen (n + 1) s + Multiset.map (Multiset.cons a) (Multiset.powersetLen n s)

@[simp]

theorem Multiset.mem_powersetLen {α : Type u_1} {n : ℕ} {s : Multiset α} {t : Multiset α} : s ∈ Multiset.powersetLen n t ↔ s ≤ t ∧ ↑Multiset.card s = n

@[simp]

theorem Multiset.card_powersetLen {α : Type u_1} (n : ℕ) (s : Multiset α) : ↑Multiset.card (Multiset.powersetLen n s) = Nat.choose (↑Multiset.card s) n

theorem Multiset.powersetLen_le_powerset {α : Type u_1} (n : ℕ) (s : Multiset α) : Multiset.powersetLen n s ≤ Multiset.powerset s

theorem Multiset.powersetLen_mono {α : Type u_1} (n : ℕ) {s : Multiset α} {t : Multiset α} (h : s ≤ t) : Multiset.powersetLen n s ≤ Multiset.powersetLen n t

@[simp]

theorem Multiset.powersetLen_empty {α : Type u_2} (n : ℕ) {s : Multiset α} (h : ↑Multiset.card s < n) : Multiset.powersetLen n s = 0

@[simp]

theorem Multiset.powersetLen_card_add {α : Type u_1} (s : Multiset α) {i : ℕ} (hi : 0 < i) : Multiset.powersetLen (↑Multiset.card s + i) s = 0

theorem Multiset.powersetLen_map {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) : Multiset.powersetLen n (Multiset.map f s) = Multiset.map (Multiset.map f) (Multiset.powersetLen n s)

theorem Multiset.pairwise_disjoint_powersetLen {α : Type u_1} (s : Multiset α) : Pairwise fun i j => Multiset.Disjoint (Multiset.powersetLen i s) (Multiset.powersetLen j s)

theorem Multiset.bind_powerset_len {α : Type u_2} (S : Multiset α) : (Multiset.bind (Multiset.range (↑Multiset.card S + 1)) fun k => Multiset.powersetLen k S) = Multiset.powerset S

@[simp]

theorem Multiset.nodup_powerset {α : Type u_1} {s : Multiset α} : Multiset.Nodup (Multiset.powerset s) ↔ Multiset.Nodup s

theorem Multiset.Nodup.ofPowerset {α : Type u_1} {s : Multiset α} : Multiset.Nodup (Multiset.powerset s) → Multiset.Nodup s

Alias of the forward direction of Multiset.nodup_powerset.

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

Alias of the reverse direction of Multiset.nodup_powerset.

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