Theorems · Definition · combinatorics
Finset.equivFin
{α : Type u_1} → (s : Finset α) → ↥s ≃ Fin s.cardNoncomputable equivalence between a finset s coerced to a type and Fin #s.
- Defined in
- Mathlib.Data.Fintype.EquivFin
- Cited by
- 15 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
- Equivstatement · cited by 8,337
- Finset.cardstatement · cited by 2,327
- Fintype.equivFinOfCardEqproof · cited by 22
Cited by16
Results whose statement or proof uses this declaration.
- PolynomialLaw.φproof · cited by 14
- Module.FinitePresentation.exists_finproof · cited by 4
- PolynomialLaw.range_φproof · cited by 3
- PolynomialLaw.isCompat_applyproof · cited by 2
- MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_memproof · cited by 2
- Finset.card_eq_of_equiv_finproof · cited by 2
- Finpartition.IsEquipartition.exists_partsEquivproof · cited by 1
- Submodule.mem_span_set'proof · cited by 1
- MeasureTheory.addContent_le_sum_of_subset_sUnionproof · cited by 1
- MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnionproof · cited by 1
- MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnionproof · cited by 1
- TopologicalSpace.IsOpenCover.exists_finite_clopen_coverproof · cited by 1