Theorems · Definition · order theory
Set.Finite.toFinset
{α : Type u} → {s : Set α} → s.Finite → Finset αUsing choice, get the Finset that represents this Set.
- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 351 results in Mathlib
- Foundations
- Depth 66 from the axioms, rests on 983 definitions · 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.
- Setstatement and proof · cited by 53,352
- Finsetstatement · cited by 13,712
- Set.Finitestatement and proof · cited by 1,814
- Set.toFinsetproof · cited by 217
Cited by376
Results whose statement or proof uses this declaration.
- Summable.hasSumproof · cited by 184
- Set.Finite.coe_toFinsetstatement · cited by 124
- Finset.preimageproof · cited by 108
- MeasureTheory.SimpleFunc.rangeproof · cited by 97
- Multipliable.hasProdproof · cited by 88
- Nat.nthproof · cited by 84
- Set.Finite.mem_toFinsetstatement · cited by 74
- Finsupp.equivFunOnFiniteproof · cited by 50
- MvPowerSeries.truncTotalproof · cited by 28
- Finset.VAddAntidiagonalproof · cited by 27
- Set.Finite.toFinset.congr_simpstatement and proof · cited by 24
- Finset.antidiagonalproof · cited by 23
Showing the 200 most cited of 376.