Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Basic Properties of Real Numbers

Krzysztof Hryniewiecki
Warsaw University
Supported by RPBP.III-24.C1.


Basic facts of arithmetics of real numbers are presented: definitions and properties of the complement element, the inverse element, subtraction and division; some basic properties of the set REAL (e.g. density), and the scheme of separation for sets of reals.

MML Identifier: REAL_1

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

Contents (PDF format)


[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[3] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[4] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received January 8, 1989

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