[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.

http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml

Thanks Andrei!

Tobias





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