@[simp]
theorem
Fintype.card_finset
{α : Type u_1}
[Fintype α]
:
Fintype.card (Finset α) = 2 ^ Fintype.card α
@[simp]
@[simp]
theorem
Finset.powerset_eq_univ
{α : Type u_1}
[Fintype α]
{s : Finset α}
:
Finset.powerset s = Finset.univ ↔ s = Finset.univ
@[simp]
theorem
Finset.mem_powerset_len_univ_iff
{α : Type u_1}
[Fintype α]
{s : Finset α}
{k : ℕ}
:
s ∈ Finset.powersetLen k Finset.univ ↔ Finset.card s = k
@[simp]
theorem
Finset.univ_filter_card_eq
(α : Type u_2)
[Fintype α]
(k : ℕ)
:
Finset.filter (fun s => Finset.card s = k) Finset.univ = Finset.powersetLen k Finset.univ
@[simp]
theorem
Fintype.card_finset_len
{α : Type u_1}
[Fintype α]
(k : ℕ)
:
Fintype.card { s // Finset.card s = k } = Nat.choose (Fintype.card α) k
@[simp]