Theorems · Definition · combinatorics
Set.toFinset
{α : Type u_1} → (s : Set α) → [Fintype ↑s] → Finset αConstruct a finset enumerating a set s, given a Fintype instance.
- Defined in
- Mathlib.Data.Fintype.Sets
- Cited by
- 217 results in Mathlib
- Foundations
- Depth 27 from the axioms, rests on 171 definitions · uses propext, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Finsetstatement · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Finset.univproof · cited by 3,473
- Finset.mapproof · cited by 747
- Function.Embedding.subtypeproof · cited by 128
Cited by235
Results whose statement or proof uses this declaration.
- Set.Finite.toFinsetproof · cited by 351
- Summable.hasSumproof · cited by 184
- SimpleGraph.edgeFinsetproof · cited by 116
- Multipliable.hasProdproof · cited by 88
- SimpleGraph.neighborFinsetproof · cited by 72
- Set.toFinset_cardstatement · cited by 63
- Set.coe_toFinsetstatement · cited by 51
- Set.mem_toFinsetstatement · cited by 47
- Set.toFinset_congrstatement and proof · cited by 33
- Multiset.toEnumFinsetproof · cited by 24
- Fintype.card_subtype_complproof · cited by 16
- Finset.toFinset_coestatement · cited by 16
Showing the 200 most cited of 235.