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

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.