Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Cardinal Numbers

Grzegorz Bancerek

Warsaw University, Bialystok

Supported by RPBP.III24.C1.
Summary.

We present the choice function rule in the beginning of the article.
In the main part of the article we formalize the base of cardinal theory.
In the first section we introduce the concept of cardinal numbers and
order relations between them. We present here CantorBernstein theorem and
other properties of order relation of cardinals.
In the second section we show that every set has cardinal number equipotence
to it. We introduce notion of alephs and we deal with the concept of finite
set. At the end of the article we show two schemes of cardinal induction.
Some definitions are based on [9] and [10].
MML Identifier:
CARD_1
The terminology and notation used in this paper have been
introduced in the following articles
[11]
[7]
[13]
[12]
[1]
[14]
[6]
[4]
[2]
[3]
[5]
[8]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Grzegorz Bancerek.
Sequences of ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Grzegorz Bancerek.
The well ordering relations.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Grzegorz Bancerek.
Zermelo theorem and axiom of choice.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Agata Darmochwal.
Finite sets.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Wojciech Guzicki and Pawel Zbierski.
\em Podstawy teorii mnogosci.
PWN, War\sza\wa, 1978.
 [10]
Kazimierz Kuratowski and Andrzej Mostowski.
\em Teoria mnogosci.
PTM, Wroc\law, 1952.
 [11]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [12]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [13]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [14]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received September 19, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]