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)
theorem
multiset.powerset_aux'_perm
{α : Type u_1}
{l₁ l₂ : list α} :
l₁ ~ l₂ → multiset.powerset_aux' l₁ ~ multiset.powerset_aux' l₂
theorem
multiset.powerset_aux_perm
{α : Type u_1}
{l₁ l₂ : list α} :
l₁ ~ l₂ → multiset.powerset_aux l₁ ~ 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
theorem
multiset.map_single_le_powerset
{α : Type u_1}
(s : multiset α) :
multiset.map (λ (a : α), a :: 0) s ≤ s.powerset
theorem
multiset.revzip_powerset_aux_perm
{α : Type u_1}
{l₁ l₂ : list α} :
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.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)
theorem
multiset.powerset_len_aux_perm
{α : Type u_1}
{n : ℕ}
{l₁ l₂ : list α} :
l₁ ~ l₂ → multiset.powerset_len_aux n l₁ ~ 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 :: 0
@[simp]
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.card_powerset_len
{α : Type u_1}
(n : ℕ)
(s : multiset α) :
(multiset.powerset_len n s).card = s.card.choose n
theorem
multiset.powerset_len_le_powerset
{α : Type u_1}
(n : ℕ)
(s : multiset α) :
multiset.powerset_len n s ≤ s.powerset
theorem
multiset.powerset_len_mono
{α : Type u_1}
(n : ℕ)
{s t : multiset α} :
s ≤ t → multiset.powerset_len n s ≤ multiset.powerset_len n t