Theorems · Definition · order theory
Set.Finite.fintype
{α : Type u} → {s : Set α} → s.Finite → Fintype ↑sA finite set coerced to a type is a Fintype.
This is the Fintype projection for a Set.Finite.
Note that because Finite isn't a typeclass, this definition will not fire if it
is made into an instance
- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Fintypestatement · cited by 7,736
- Set.Elemstatement · cited by 7,166
- Set.Finitestatement and proof · cited by 1,814
- Nonempty.someproof · cited by 340
- Set.Finite.nonempty_fintypeproof · cited by 4
Cited by38
Results whose statement or proof uses this declaration.
- Submodule.eq_top_of_finrank_eqproof · cited by 15
- ZLattice.rankproof · cited by 5
- Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegInproof · cited by 5
- finprod_le_finprodproof · cited by 5
- Filter.mem_iInf_of_iInterproof · cited by 5
- Set.Finite.card_lt_cardproof · cited by 4
- Set.Finite.encard_eq_coe_toFinset_cardproof · cited by 4
- Cardinal.card_lt_card_of_right_finiteproof · cited by 3
- MDifferentiableWithinAt.sum_section_of_locallyFiniteproof · cited by 3
- Nat.card_image_of_injOnproof · cited by 3
- Set.Finite.isCompact_convexHullproof · cited by 3
- ContMDiffWithinAt.sum_section_of_locallyFiniteproof · cited by 3