Theorems · Inductive type · combinatorics
FinEnum
Sort u_1 → Sort (max 1 u_1)
FinEnum α means that α is finite and can be enumerated in some order,
i.e. α has an explicit bijection with Fin n for some n.
- Defined in
- Mathlib.Data.FinEnum
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 0 from the axioms · 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 by41
Results whose statement or proof uses this declaration.
- FinEnum.cardstatement and proof · cited by 32
- FinEnum.equivstatement and proof · cited by 9
- FinEnum.toListstatement and proof · cited by 4
- FinEnum.card_eq_fintypeCardstatement and proof · cited by 4
- FinEnum.insertNonestatement and proof · cited by 3
- FinEnum.recEmptyOptionstatement and proof · cited by 3
- FinEnum.recEmptyOption.eq_defstatement and proof · cited by 2
- FinEnum.mem_toListstatement and proof · cited by 1
- FinEnum.ofListstatement · cited by 1
- List.Pi.enumstatement and proof · cited by 1
- List.mem_pi_toListstatement and proof · cited by 1
- FinEnum.card_eq_zerostatement and proof · cited by 1