Theorems · Definition · combinatorics
Finset.powersetCard
{α : Type u_1} → ℕ → Finset α → Finset (Finset α)Given an integer n and a finset s, then powersetCard n s is the finset of subsets of s
of cardinality n.
- Defined in
- Mathlib.Data.Finset.Powerset
- Cited by
- 60 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.valproof · cited by 438
- Multiset.powersetCardproof · cited by 29
- Multiset.pmapproof · cited by 16
Cited by62
Results whose statement or proof uses this declaration.
- MvPolynomial.esymmproof · cited by 31
- Finset.mem_powersetCardstatement · cited by 14
- Finset.card_powersetCardstatement · cited by 10
- Finset.fallingproof · cited by 8
- Finset.pairwise_disjoint_powersetCardstatement and proof · cited by 5
- Finset.powersetCard_eq_filterstatement · cited by 4
- Finset.mem_powersetCard_univstatement · cited by 3
- Finset.powersetCard_nonemptystatement · cited by 3
- Finset.powerset_card_disjiUnionstatement and proof · cited by 3
- Finset.esymm_map_valstatement and proof · cited by 3
- Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_chooseproof · cited by 2
- Finset.univ_filter_card_eqstatement · cited by 2