Theorems · Inductive type · combinatorics
Finset
Type u_4 → Type u_4
Finset α is the type of finite sets of elements of α. It is implemented
as a multiset (a list up to permutation) which has no duplicate elements.
- Defined in
- Mathlib.Data.Finset.Defs
- Cited by
- 13,712 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by14,738
Results whose statement or proof uses this declaration.
- Finset.sumstatement and proof · cited by 5,195
- Finset.univstatement · cited by 3,473
- Finset.prodstatement and proof · cited by 2,356
- Finset.cardstatement and proof · cited by 2,327
- Finset.sum_congrstatement and proof · cited by 2,323
- Finset.rangestatement · cited by 1,341
- Finset.Nonemptystatement and proof · cited by 1,001
- Finset.filterstatement and proof · cited by 949
- Finset.imagestatement and proof · cited by 910
- Finsupp.supportstatement · cited by 828
- Finset.mapstatement and proof · cited by 747
- Finset.prod_congrstatement and proof · cited by 646
Showing the 200 most cited of 14,738.