Some Properties of Dyadic Numbers and Intervals

Jozef Bialas

Lodz University

Yatsuka Nakamura

Shinshu University, Nagano

Summary.

The article is the second part of a paper proving the fundamental Urysohn Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into two parts. In the first part, we introduce some definitions and theorems concerning properties of intervals; in the second we prove some of properties of dyadic numbers used in proving Urysohn Lemma.

MML Identifier: URYSOHN2

Contents (PDF format)

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. Properties of the intervals of real numbers. Journal of Formalized Mathematics, 5, 1993.

[5] Jozef Bialas. Some properties of the intervals. Journal of Formalized Mathematics, 6, 1994.

[6] Jozef Bialas and Yatsuka Nakamura. Dyadic numbers and T$_4$ topological spaces. Journal of Formalized Mathematics, 7, 1995.

[7] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Scalar multiple of Riemann definite integral. Journal of Formalized Mathematics, 11, 1999.

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

[9] Rafal Kwiatek. Factorial and Newton coefficients. Journal of Formalized Mathematics, 2, 1990.

[10] Jan Popiolek. Some properties of functions modul and signum. Journal of Formalized Mathematics, 1, 1989.

[11] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

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

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