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.
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]