Ordinals Cardinals (Q40628)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Ordinals_and_Cardinals
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Ordinals Cardinals |
AFP entry Ordinals_and_Cardinals |
Statements
Andrei Popescu
0 references
We develop a basic theory of ordinals and cardinals in Isabelle/HOL, up to the point where some cardinality facts relevant for the “working mathematician” become available. Unlike in set theory, here we do not have at hand canonical notions of ordinal and cardinal. Therefore, here an ordinal is merely a well-order relation and a cardinal is an ordinal minim w.r.t. order embedding on its field.
0 references
1 September 2009
0 references
Ordinals and Cardinals (English)
0 references
