Basic Properties of Extended Real Numbers

Noboru Endou

Shinshu University, Nagano

Katsumi Wasaki

Shinshu University, Nagano

Yasunari Shidama

Shinshu University, Nagano

Summary.

We introduce product, quotient and absolute value, and we prove some basic properties of extended real numbers.

MML Identifier: EXTREAL1

Contents (PDF format)

1. Preliminaries
2. Operations of Multiplication, Quotient and Absolute Value on Extended Real Numbers

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] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.