Theorems · Theorem · logic and foundations
Ordinal.cof_eq_aleph0_of_isSuccLimit
∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → o < Ordinal.omega 1 → o.cof = Cardinal.aleph0A countable limit ordinal has cofinality ℵ₀.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- LE.le.transproof · cited by 3,151
- Cardinalstatement and proof · cited by 2,598
- Ordinalstatement and proof · cited by 1,688
- OrderEmbeddingstatement · cited by 619
- Cardinal.aleph0statement · cited by 521
- LE.le.antisymmproof · cited by 507
- Cardinal.ordproof · cited by 266
- Order.IsSuccLimitstatement and proof · cited by 255
- Ordinal.cofstatement · cited by 125
- Ordinal.omegastatement and proof · cited by 60
- Cardinal.ord_alephproof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- Ordinal.cof_omega0proof · cited by 2