Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
Some Properties of Real Numbers
Operations: min, max, square, and square root

Andrzej Trybulec

Warsaw University, Bialystok

Czeslaw Bylinski

Warsaw University, Bialystok
Summary.

We define the following operations on real numbers:
$max(x,y)$, $min(x,y)$, $x^2$, $\sqrt{x}$.
We prove basic properties of introduced operations.
A number of auxiliary theorems absent in [2] and
[3] is proved.
Supported by RPBP.III24.C1.
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[6]
[1]
[5]
[3]
Contents (PDF format)
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Jan Popiolek.
Some properties of functions modul and signum.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [5]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [6]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received November 16, 1989
[
Download a postscript version,
MML identifier index,
Mizar home page]