Theorems · Definition · logic and foundations
Cardinal
Type (u + 1)
Cardinal.{u} is the type of cardinal numbers in Type u,
defined as the quotient of Type u by existence of an equivalence
(a bijection with explicit inverse).
- Defined in
- Mathlib.SetTheory.Cardinal.Defs
- Cited by
- 2,598 results in Mathlib
- Foundations
- Depth 18 from the axioms, rests on 69 definitions · uses Quot.sound
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 by2,840
Results whose statement or proof uses this declaration.
- Cardinal.mkstatement · cited by 942
- Cardinal.liftstatement and proof · cited by 583
- Cardinal.aleph0statement · cited by 521
- Module.rankstatement · cited by 496
- Cardinal.IsRegularstatement · cited by 282
- Cardinal.ordstatement and proof · cited by 266
- Cardinal.lift_idstatement and proof · cited by 163
- Cardinal.toNatstatement · cited by 153
- Ordinal.cofstatement · cited by 125
- Ordinal.cardstatement · cited by 122
- HasCardinalLTstatement and proof · cited by 99
- Cardinal.toENatstatement and proof · cited by 92
Showing the 200 most cited of 2,840.