mathlib3 documentation

data.multiset.powerset

The powerset of a multiset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

powerset #

source
def multiset.powerset_aux {α : 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 (using sublists_aux), as multisets.

Equations
source
theorem multiset.powerset_aux_eq_map_coe {α : Type u_1} {l : list α} :
multiset.powerset_aux l = list.map coe l.sublists
source
@[simp]
theorem multiset.mem_powerset_aux {α : Type u_1} {l : list α} {s : multiset α} :
s ∈ multiset.powerset_aux l ↔ s ≤ ↑l
source
def multiset.powerset_aux' {α : 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
source
theorem multiset.powerset_aux_perm_powerset_aux' {α : Type u_1} {l : list α} :
multiset.powerset_aux l ~ multiset.powerset_aux' l
source
@[simp]
theorem multiset.powerset_aux'_nil {α : Type u_1} :
multiset.powerset_aux' list.nil = [0]
source
@[simp]
theorem multiset.powerset_aux'_cons {α : Type u_1} (a : α) (l : list α) :
multiset.powerset_aux' (a :: l) = multiset.powerset_aux' l ++ list.map (multiset.cons a) (multiset.powerset_aux' l)
source
theorem multiset.powerset_aux'_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
multiset.powerset_aux' l₁ ~ multiset.powerset_aux' l₂
source
theorem multiset.powerset_aux_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
multiset.powerset_aux l₁ ~ multiset.powerset_aux l₂
source
def multiset.powerset {α : Type u_1} (s : multiset α) :
multiset (multiset α)

The power set of a multiset.

Equations
source
theorem multiset.powerset_coe {α : Type u_1} (l : list α) :
↑l.powerset = ↑(list.map coe l.sublists)
source
@[simp]
theorem multiset.powerset_coe' {α : Type u_1} (l : list α) :
↑l.powerset = ↑(list.map coe l.sublists')
source
@[simp]
theorem multiset.powerset_zero {α : Type u_1} :
0.powerset = {0}
source
@[simp]
theorem multiset.powerset_cons {α : Type u_1} (a : α) (s : multiset α) :
(a ::ₘ s).powerset = s.powerset + multiset.map (multiset.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 α) :
multiset.map has_singleton.singleton s ≤ s.powerset
source
@[simp]
theorem multiset.card_powerset {α : Type u_1} (s : multiset α) :
⇑multiset.card s.powerset = 2 ^ ⇑multiset.card s
source
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
source
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
source
theorem multiset.revzip_powerset_aux_lemma {α : Type u_1} [decidable_eq α] (l : list α) {l' : list (multiset α)} (H : ∀ ⦃x : multiset α × multiset α⦄, x ∈ l'.revzip → x.fst + x.snd = ↑l) :
l'.revzip = list.map (λ (x : multiset α), (x, ↑l - x)) l'
source
theorem multiset.revzip_powerset_aux_perm_aux' {α : Type u_1} {l : list α} :
(multiset.powerset_aux l).revzip ~ (multiset.powerset_aux' l).revzip
source
theorem multiset.revzip_powerset_aux_perm {α : Type u_1} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
(multiset.powerset_aux l₁).revzip ~ (multiset.powerset_aux l₂).revzip

powerset_len #

source
def multiset.powerset_len_aux {α : Type u_1} (n : ℕ) (l : 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
source
theorem multiset.powerset_len_aux_eq_map_coe {α : Type u_1} {n : ℕ} {l : list α} :
multiset.powerset_len_aux n l = list.map coe (list.sublists_len n l)
source
@[simp]
theorem multiset.mem_powerset_len_aux {α : Type u_1} {n : ℕ} {l : list α} {s : multiset α} :
s ∈ multiset.powerset_len_aux n l ↔ s ≤ ↑l ∧ ⇑multiset.card s = n
source
@[simp]
theorem multiset.powerset_len_aux_zero {α : Type u_1} (l : list α) :
multiset.powerset_len_aux 0 l = [0]
source
@[simp]
theorem multiset.powerset_len_aux_nil {α : Type u_1} (n : ℕ) :
multiset.powerset_len_aux (n + 1) list.nil = list.nil
source
@[simp]
theorem multiset.powerset_len_aux_cons {α : Type u_1} (n : ℕ) (a : α) (l : list α) :
multiset.powerset_len_aux (n + 1) (a :: l) = multiset.powerset_len_aux (n + 1) l ++ list.map (multiset.cons a) (multiset.powerset_len_aux n l)
source
theorem multiset.powerset_len_aux_perm {α : Type u_1} {n : ℕ} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
multiset.powerset_len_aux n l₁ ~ multiset.powerset_len_aux n l₂
source
def multiset.powerset_len {α : Type u_1} (n : ℕ) (s : multiset α) :
multiset (multiset α)

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

Equations
source
theorem multiset.powerset_len_coe' {α : Type u_1} (n : ℕ) (l : list α) :
multiset.powerset_len n ↑l = ↑(multiset.powerset_len_aux n l)
source
theorem multiset.powerset_len_coe {α : Type u_1} (n : ℕ) (l : list α) :
multiset.powerset_len n ↑l = ↑(list.map coe (list.sublists_len n l))
source
@[simp]
theorem multiset.powerset_len_zero_left {α : Type u_1} (s : multiset α) :
multiset.powerset_len 0 s = {0}
source
theorem multiset.powerset_len_zero_right {α : Type u_1} (n : ℕ) :
multiset.powerset_len (n + 1) 0 = 0
source
@[simp]
theorem multiset.powerset_len_cons {α : Type u_1} (n : ℕ) (a : α) (s : multiset α) :
multiset.powerset_len (n + 1) (a ::ₘ s) = multiset.powerset_len (n + 1) s + multiset.map (multiset.cons a) (multiset.powerset_len n s)
source
@[simp]
theorem multiset.mem_powerset_len {α : Type u_1} {n : ℕ} {s t : multiset α} :
s ∈ multiset.powerset_len n t ↔ s ≤ t ∧ ⇑multiset.card s = n
source
@[simp]
theorem multiset.card_powerset_len {α : Type u_1} (n : ℕ) (s : multiset α) :
⇑multiset.card (multiset.powerset_len n s) = (⇑multiset.card s).choose n
source
theorem multiset.powerset_len_le_powerset {α : Type u_1} (n : ℕ) (s : multiset α) :
multiset.powerset_len n s ≤ s.powerset
source
theorem multiset.powerset_len_mono {α : Type u_1} (n : ℕ) {s t : multiset α} (h : s ≤ t) :
multiset.powerset_len n s ≤ multiset.powerset_len n t
source
@[simp]
theorem multiset.powerset_len_empty {α : Type u_1} (n : ℕ) {s : multiset α} (h : ⇑multiset.card s < n) :
multiset.powerset_len n s = 0
source
@[simp]
theorem multiset.powerset_len_card_add {α : Type u_1} (s : multiset α) {i : ℕ} (hi : 0 < i) :
multiset.powerset_len (⇑multiset.card s + i) s = 0
source
theorem multiset.powerset_len_map {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (s : multiset α) :
multiset.powerset_len n (multiset.map f s) = multiset.map (multiset.map f) (multiset.powerset_len n s)
source
theorem multiset.pairwise_disjoint_powerset_len {α : Type u_1} (s : multiset α) :
pairwise (λ (i j : ℕ), (multiset.powerset_len i s).disjoint (multiset.powerset_len j s))
source
theorem multiset.bind_powerset_len {α : Type u_1} (S : multiset α) :
(multiset.range (⇑multiset.card S + 1)).bind (λ (k : ℕ), multiset.powerset_len k S) = S.powerset
source
@[simp]
theorem multiset.nodup_powerset {α : Type u_1} {s : multiset α} :
s.powerset.nodup ↔ s.nodup
source
theorem multiset.nodup.of_powerset {α : Type u_1} {s : multiset α} :
s.powerset.nodup → s.nodup

Alias of the forward direction of multiset.nodup_powerset.

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
@[protected]
theorem multiset.nodup.powerset_len {α : Type u_1} {n : ℕ} {s : multiset α} (h : s.nodup) :
(multiset.powerset_len n s).nodup