Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
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.
The terminology and notation used in this paper have been
introduced in the following articles
[1]
[5]
[2]
[3]
[4]

Preliminaries

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.
Received September 7, 2000
[
Download a postscript version,
MML identifier index,
Mizar home page]