Cardinal Numbers

Grzegorz Bancerek

Warsaw University, Bialystok

Supported by RPBP.III-24.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 Cantor-Bernstein 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

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.