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

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.