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.