Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Ordinal Arithmetics


Grzegorz Bancerek
Warsaw University, Bialystok

Summary.

At the beginning the article contains some auxiliary theorems concerning the constructors defined in papers [1] and [2]. Next simple properties of addition and multiplication of ordinals are shown, e.g. associativity of addition. Addition and multiplication of a transfinite sequence of ordinals and a ordinal are also introduced here. The goal of the article is the proof that the distributivity of multiplication wrt addition and the associativity of multiplication hold. Additionally new binary functors of ordinals are introduced: subtraction, exact division, and remainder and some of their basic properties are presented.

MML Identifier: ORDINAL3

The terminology and notation used in this paper have been introduced in the following articles [5] [6] [7] [3] [1] [4] [2]

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Beata Padlewska. Families of sets. Journal of Formalized Mathematics, 1, 1989.
[5] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[6] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[7] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received March 1, 1990


[ Download a postscript version, MML identifier index, Mizar home page]