Equalities and Inequalities in Real Numbers

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Equalities and Inequalities in Real Numbers

Andrzej Kondracki: Warsaw University

Summary.

The aim of the article is to give a number of useful theorems concerning equalities and inequalities in real numbers. Some of the theorems are extensions of [2] theorems, others were found to be needed in practice.

MML Identifier: REAL_2

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

Contents (PDF format)

Bibliography

[1] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[4] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received September 5, 1990

[ Download a postscript version, MML identifier index, Mizar home page]