[isabelle] New AFP entry: Ordinals and Cardinals by Andrei Popescu

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.


Thanks Andrei!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.