[isabelle] New AFP entry: Ordinals and Cardinals by Andrei Popescu
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP entry: Ordinals and Cardinals by Andrei Popescu
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Wed, 09 Sep 2009 18:39:02 +0200
- User-agent: Thunderbird 22.214.171.124 (Macintosh/20090812)
Title: Ordinals and Cardinals
Author: Andrei Popescu
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and