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.III24.C1.
Summary.

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)
Bibliography
 [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]