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].

MML Identifier: EXTREAL2

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

Contents (PDF format)

  1. Preliminaries
  2. Basic Properties of abs for Extended Real Numbers
  3. 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]