The powerset of a multiset #
powerset #
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
- multiset.powerset_aux l = 0 :: l.sublists_aux (λ (x : list α) (y : list (multiset α)), ↑x :: y)
@[simp]
theorem
multiset.mem_powerset_aux
{α : Type u_1}
{l : list α}
{s : multiset α} :
s ∈ multiset.powerset_aux l ↔ s ≤ ↑l
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]
@[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)
The power set of a multiset.
Equations
- s.powerset = quot.lift_on s (λ (l : list α), ↑(multiset.powerset_aux l)) multiset.powerset._proof_1
@[simp]
theorem
multiset.powerset_cons
{α : Type u_1}
(a : α)
(s : multiset α) :
(a ::ₘ s).powerset = s.powerset + multiset.map (multiset.cons a) s.powerset
@[simp]
theorem
multiset.card_powerset
{α : Type u_1}
(s : multiset α) :
⇑multiset.card s.powerset = 2 ^ ⇑multiset.card s
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 #
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
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)
@[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
@[simp]
theorem
multiset.powerset_len_aux_zero
{α : Type u_1}
(l : list α) :
multiset.powerset_len_aux 0 l = [0]
@[simp]
@[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)
powerset_len n s
is the multiset of all submultisets of s
of length n
.
Equations
- multiset.powerset_len n s = quot.lift_on s (λ (l : list α), ↑(multiset.powerset_len_aux n l)) _
theorem
multiset.powerset_len_coe
{α : Type u_1}
(n : ℕ)
(l : list α) :
multiset.powerset_len n ↑l = ↑(list.map coe (list.sublists_len n l))
@[simp]
theorem
multiset.powerset_len_zero_left
{α : Type u_1}
(s : multiset α) :
multiset.powerset_len 0 s = {0}
theorem
multiset.powerset_len_zero_right
{α : Type u_1}
(n : ℕ) :
multiset.powerset_len (n + 1) 0 = 0
@[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)
@[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
@[simp]
theorem
multiset.card_powerset_len
{α : Type u_1}
(n : ℕ)
(s : multiset α) :
⇑multiset.card (multiset.powerset_len n s) = (⇑multiset.card s).choose n
theorem
multiset.powerset_len_le_powerset
{α : Type u_1}
(n : ℕ)
(s : multiset α) :
multiset.powerset_len n s ≤ s.powerset
@[simp]
theorem
multiset.powerset_len_empty
{α : Type u_1}
(n : ℕ)
{s : multiset α}
(h : ⇑multiset.card s < n) :
multiset.powerset_len n s = 0
@[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
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)
theorem
multiset.disjoint_powerset_len
{α : Type u_1}
(s : multiset α)
{i j : ℕ}
(h : i ≠ j) :
(multiset.powerset_len i s).disjoint (multiset.powerset_len j s)
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