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

Michal J. Trybulec

Warsaw University, Bialystok
Summary.

In the article the following concepts were introduced:
the set of integers (${\Bbb Z }$)
and its elements (integers),
congruences ($i_1 \equiv i_2 (\mathop{\rm mod} i_3)$),
the ceiling and floor functors ($\mathopen{\lceil} x \mathclose{\rceil}$ and
$\mathopen{\lfloor} x \mathclose{\rfloor}$), also
the fraction part of a real number (frac),
the integer division ($\div$) and remainder of integer division (mod).
The following schemes were also included:
the separation scheme ({\it SepInt}),
the schemes of integer induction ({\it Int\_Ind\_Down},
{\it Int\_Ind\_Up}, {\it Int\_Ind\_Full}),
the minimum ({\it Int\_Min}) and maximum ({\it Int\_Max}) schemes (the
existence of minimum and maximum integers enjoying a given property).
MML Identifier:
INT_1
The terminology and notation used in this paper have been
introduced in the following articles
[6]
[3]
[8]
[1]
[2]
[7]
[4]
[5]
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.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Jan Popiolek.
Some properties of functions modul and signum.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [7]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [8]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received February 7, 1990
[
Download a postscript version,
MML identifier index,
Mizar home page]