Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Ordinals and Cardinals by Andre...

Email Gateway (Aug 18 2022 at 14:02):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Apr 23 2024 at 16:19 UTC