Theorems · Inductive type · logic and foundations
Cardinal.IsRegular
Cardinal.{u_1} → PropA cardinal is regular if it is infinite and it equals its own cofinality.
- Defined in
- Mathlib.SetTheory.Cardinal.Regular
- Cited by
- 282 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 70 definitions · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement · cited by 2,598
Cited by387
Results whose statement or proof uses this declaration.
- CategoryTheory.IsCardinalFilteredstatement · cited by 69
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgumentstatement · cited by 49
- CategoryTheory.IsCardinalPresentablestatement and proof · cited by 39
- PartOrdEmb.isCardinalFilteredstatement and proof · cited by 25
- CategoryTheory.CardinalDirectedPosetstatement and proof · cited by 24
- Cardinal.IsRegular.cof_ordstatement and proof · cited by 23
- Cardinal.IsRegular.aleph0_lestatement and proof · cited by 22
- CategoryTheory.SmallObject.objstatement and proof · cited by 22
- CategoryTheory.ObjectProperty.IsCardinalFilteredGeneratorstatement · cited by 22
- CategoryTheory.isCardinalPresentablestatement and proof · cited by 20
- CategoryTheory.Functor.IsCardinalAccessiblestatement · cited by 19
- CategoryTheory.isFiltered_of_isCardinalFilteredstatement and proof · cited by 18
Showing the 200 most cited of 387.