Structures · Logic and sets
IsRegularCardinalOrder
A typeclass which expresses that the order type of a well-order equals (the initial ordinal of)
its cofinality.
If α is infinite, this implies that α is order isomorphic to Iio c.ord for some regular
cardinal c. In the informal literature, one often says that α is a regular cardinal, by abuse
of notation.
- Shape
- One type argument · adds type_lt_le_ord_cof
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Nat
- Ordinal
- Cardinal
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- Order.enum
- Order.cof_eq_cardinalMk
- Order.enum_le_of_forall_lt
- Order.ord_cof_eq_type_lt
- IsRegularCardinalOrder.type_lt_le_ord_cof
- Cardinal.ord_cardinalMk
- Order.enum_eq_iff
- Order.isNormal_enum_iff_isClub
- Order.enum.congr_simp
- Order.enum_range
- Order.enum_bot
- IsClub.isNormal_enum
- Order.type_eq_of_isCofinal
- Order.isNormal_enum_iff_dirSupClosed
- Order.enum_succ_le_of_lt
- Order.enum_anti
- Order.enum_univ
Ancestors0
No ancestors.