# The powerset of a multiset #

### powerset #

source
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 l.sublists

Instances For

source
theorem Multiset.powersetAux_eq_map_coe {α : Type u_1} {l : List α} :
powersetAux l = List.map ofList l.sublists
source
@[simp]
theorem Multiset.mem_powersetAux {α : Type u_1} {l : List α} {s : Multiset α} :
s ∈ powersetAux l ↔ s ≤ ↑l
source
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 l.sublists'

Instances For

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

The power set of a multiset.

Equations

- s.powerset = Quot.liftOn s (fun (l : List α) => ↑(Multiset.powersetAux l)) ⋯

Instances For

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

### powersetCard #

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

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

Equations

- Multiset.powersetCardAux n l = List.sublistsLenAux n l Multiset.ofList []

Instances For

source
theorem Multiset.powersetCardAux_eq_map_coe {α : Type u_1} {n : ℕ} {l : List α} :
powersetCardAux n l = List.map ofList (List.sublistsLen n l)
source
@[simp]
theorem Multiset.mem_powersetCardAux {α : Type u_1} {n : ℕ} {l : List α} {s : Multiset α} :
s ∈ powersetCardAux n l ↔ s ≤ ↑l ∧ s.card = n
source
@[simp]
theorem Multiset.powersetCardAux_zero {α : Type u_1} (l : List α) :
powersetCardAux 0 l = [0]
source
@[simp]
theorem Multiset.powersetCardAux_nil {α : Type u_1} (n : ℕ) :
powersetCardAux (n + 1) [] = []
source
@[simp]
theorem Multiset.powersetCardAux_cons {α : Type u_1} (n : ℕ) (a : α) (l : List α) :
powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)
source
theorem Multiset.powersetCardAux_perm {α : Type u_1} {n : ℕ} {l₁ l₂ : List α} (p : l₁.Perm l₂) :
(powersetCardAux n l₁).Perm (powersetCardAux n l₂)
source
def Multiset.powersetCard {α : Type u_1} (n : ℕ) (s : Multiset α) :
Multiset (Multiset α)

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

Equations

- Multiset.powersetCard n s = Quot.liftOn s (fun (l : List α) => ↑(Multiset.powersetCardAux n l)) ⋯

Instances For

source
theorem Multiset.powersetCard_coe' {α : Type u_1} (n : ℕ) (l : List α) :
powersetCard n ↑l = ↑(powersetCardAux n l)
source
theorem Multiset.powersetCard_coe {α : Type u_1} (n : ℕ) (l : List α) :
powersetCard n ↑l = ↑(List.map ofList (List.sublistsLen n l))
source
@[simp]
theorem Multiset.powersetCard_zero_left {α : Type u_1} (s : Multiset α) :
powersetCard 0 s = {0}
source
theorem Multiset.powersetCard_zero_right {α : Type u_1} (n : ℕ) :
powersetCard (n + 1) 0 = 0
source
@[simp]
theorem Multiset.powersetCard_cons {α : Type u_1} (n : ℕ) (a : α) (s : Multiset α) :
powersetCard (n + 1) (a ::ₘ s) = powersetCard (n + 1) s + map (cons a) (powersetCard n s)
source
theorem Multiset.powersetCard_one {α : Type u_1} (s : Multiset α) :
powersetCard 1 s = map singleton s
source
@[simp]
theorem Multiset.mem_powersetCard {α : Type u_1} {n : ℕ} {s t : Multiset α} :
s ∈ powersetCard n t ↔ s ≤ t ∧ s.card = n
source
@[simp]
theorem Multiset.card_powersetCard {α : Type u_1} (n : ℕ) (s : Multiset α) :
(powersetCard n s).card = s.card.choose n
source
theorem Multiset.powersetCard_le_powerset {α : Type u_1} (n : ℕ) (s : Multiset α) :
powersetCard n s ≤ s.powerset
source
theorem Multiset.powersetCard_mono {α : Type u_1} (n : ℕ) {s t : Multiset α} (h : s ≤ t) :
powersetCard n s ≤ powersetCard n t
source
@[simp]
theorem Multiset.powersetCard_eq_empty {α : Type u_2} (n : ℕ) {s : Multiset α} (h : s.card < n) :
powersetCard n s = 0
source
theorem Multiset.powersetCard_card_add {α : Type u_1} (s : Multiset α) {i : ℕ} (hi : 0 < i) :
powersetCard (s.card + i) s = 0
source
theorem Multiset.powersetCard_map {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : Multiset α) :
powersetCard n (map f s) = map (map f) (powersetCard n s)
source
theorem Multiset.pairwise_disjoint_powersetCard {α : Type u_1} (s : Multiset α) :
_root_.Pairwise fun (i j : ℕ) => Disjoint (powersetCard i s) (powersetCard j s)
source
theorem Multiset.bind_powerset_len {α : Type u_2} (S : Multiset α) :
((range (S.card + 1)).bind fun (k : ℕ) => powersetCard k S) = S.powerset
source
@[simp]
theorem Multiset.nodup_powerset {α : Type u_1} {s : Multiset α} :
s.powerset.Nodup ↔ s.Nodup
source
theorem Multiset.Nodup.powerset {α : Type u_1} {s : Multiset α} :
s.Nodup → s.powerset.Nodup

Alias of the reverse direction of `Multiset.nodup_powerset`.

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

Alias of the forward direction of `Multiset.nodup_powerset`.

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