Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
Some Properties of Extended Real Numbers Operations: abs, min and max

Noboru Endou

Shinshu University, Nagano

Katsumi Wasaki

Shinshu University, Nagano

Yasunari Shidama

Shinshu University, Nagano
Summary.

In this article, we extend
some properties concerning real numbers to extended real numbers.
Almost all properties included in this article are extended properties of other
articles: [10], [7],
[9], [11] and [8].
The terminology and notation used in this paper have been
introduced in the following articles
[1]
[9]
[11]
[2]
[3]
[4]
[5]
[6]

Preliminaries

Basic Properties of abs for Extended Real Numbers

Definitions of min, max for Extended Real Numbers and their Basic Properties
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Jozef Bialas.
Infimum and supremum of the set of real numbers. Measure theory.
Journal of Formalized Mathematics,
2, 1990.
 [3]
Jozef Bialas.
Series of positive real numbers. Measure theory.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Jozef Bialas.
Some properties of the intervals.
Journal of Formalized Mathematics,
6, 1994.
 [5]
Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.
Basic properties of extended real numbers.
Journal of Formalized Mathematics,
12, 2000.
 [6]
Noboru Endou, Katsumi Wasaki, and Yasunari Shidama.
Definitions and basic properties of measurable functions.
Journal of Formalized Mathematics,
12, 2000.
 [7]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Andrzej Kondracki.
Equalities and inequalities in real numbers.
Journal of Formalized Mathematics,
2, 1990.
 [9]
Jan Popiolek.
Some properties of functions modul and signum.
Journal of Formalized Mathematics,
1, 1989.
 [10]
Andrzej Trybulec.
Strong arithmetic of real numbers.
Journal of Formalized Mathematics,
Addenda, 1989.
 [11]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
Journal of Formalized Mathematics,
1, 1989.
Received September 15, 2000
[
Download a postscript version,
MML identifier index,
Mizar home page]