The powerset of a finset
powerset
theorem
finset.powerset_insert
{α : Type u_1}
[decidable_eq α]
(s : finset α)
(a : α) :
(has_insert.insert a s).powerset = s.powerset ∪ finset.image (has_insert.insert a) s.powerset
Given an integer n and a finset s, then powerset_len n s is the finset of subsets of s
of cardinality n.
Equations
- finset.powerset_len n s = {val := multiset.pmap finset.mk (multiset.powerset_len n s.val) _, nodup := _}
@[simp]
theorem
finset.powerset_len_mono
{α : Type u_1}
{n : ℕ}
{s t : finset α} :
s ⊆ t → finset.powerset_len n s ⊆ finset.powerset_len n t
@[simp]
theorem
finset.card_powerset_len
{α : Type u_1}
(n : ℕ)
(s : finset α) :
(finset.powerset_len n s).card = s.card.choose n