| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
Ordinals and Cardinals
| Title: | Ordinals and Cardinals |
| Author: | Andrei Popescu |
| Submission date: | 2009-09-01 |
| Abstract: | 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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |