Theorems · Inductive type · logic and foundations

IsRegularCardinalOrder

(α : Type u_2) → [inst : LinearOrder α] → [WellFoundedLT α] → Prop

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.

Defined in

Mathlib.SetTheory.Cardinal.Cofinality.Enum

Cited by

17 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

LinearOrderWellFoundedLT