Theorems · Definition · logic and foundations
Ordinal.cof
Ordinal.{u} → Cardinal.{u}The cofinality on an ordinal is the Order.cof of any isomorphic linear order.
In particular, cof 0 = 0 and cof (succ o) = 1.
- Cited by
- 125 results in Mathlib
- Foundations
- Depth 83 from the axioms, rests on 1,028 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderproof · cited by 8,572
- Cardinalstatement · cited by 2,598
- Ordinalstatement and proof · cited by 1,688
- WellFoundedLTproof · cited by 491
- Order.cofproof · cited by 86
- Ordinal.liftOnWellOrderproof · cited by 1
Cited by134
Results whose statement or proof uses this declaration.
- Cardinal.IsRegular.cof_ordstatement · cited by 23
- Ordinal.IsFundamentalSequenceproof · cited by 12
- Ordinal.cof_typestatement · cited by 9
- Ordinal.lift_cofstatement and proof · cited by 8
- Ordinal.lift_iSup_lt_of_lt_cofstatement and proof · cited by 8
- Ordinal.cof_map_of_isNormalstatement and proof · cited by 7
- Ordinal.cof_toTypestatement and proof · cited by 7
- Ordinal.cof_zerostatement · cited by 7
- Ordinal.lift_iSup_add_one_lt_of_lt_cofstatement and proof · cited by 6
- Cardinal.isRegular_succproof · cited by 6
- Cardinal.IsInaccessible.univproof · cited by 6
- Ordinal.iSup_lt_of_lt_cofstatement and proof · cited by 5