Theorems · Theorem · combinatorics
finite_or_infinite
∀ (α : Sort u_3), Finite α ∨ Infinite α
- Defined in
- Mathlib.Data.Finite.Defs
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finitestatement · cited by 3,029
- Infinitestatement · cited by 352
- not_finite_iff_infiniteproof · cited by 8
Cited by50
Results whose statement or proof uses this declaration.
- Nat.card_unitsproof · cited by 6
- Cardinal.mk_list_le_maxproof · cited by 4
- Field.nonempty_algHom_of_exists_rootproof · cited by 3
- Cardinal.exists_finset_eq_cardproof · cited by 3
- Projectivization.cardproof · cited by 3
- MulAction.IsPreprimitive.isMultiplyPreprimitiveproof · cited by 2
- Group.isCyclic_prod_iffproof · cited by 2
- Module.finite_dual_iffproof · cited by 2
- Cardinal.mk_list_eq_maxproof · cited by 2
- Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_cardproof · cited by 2
- Ring.HasFiniteQuotients.finite_cardQuot_leproof · cited by 2
- Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_cardproof · cited by 2