Ordinals and Cardinals

Andrei Popescu 🌐

September 1, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

History

September 25, 2012
This entry has been discontinued because it is now part of the Isabelle distribution.

Topics

Session Ordinals_and_Cardinals

Cite

× 
@article{Ordinals_and_Cardinals-AFP,
  author  = {Andrei Popescu},
  title   = {Ordinals and Cardinals},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2009},
  note    = {\url{https://isa-afp.org/entries/Ordinals_and_Cardinals.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: